Joey Hess 77c42782d0 differentiate between concurrency enabled at command line and by git config ... The latter should not affect --batch mode.		2020-09-16 11:47:12 -04:00
..
Options.hs	differentiate between concurrency enabled at command line and by git config	2020-09-16 11:47:12 -04:00