diff options
| author | Joey Hess <joeyh@joeyh.name> | 2020-09-16 11:41:28 -0400 |
|---|---|---|
| committer | Joey Hess <joeyh@joeyh.name> | 2020-09-16 11:47:12 -0400 |
| commit | 77c42782d0bfa7e11db099dfd1ead400a8d3cb17 (patch) | |
| tree | 31ec290286c0154a9fda4d2396ddb87e8d446f86 /Types/Concurrency.hs | |
| parent | 8471df3b6dd3710ab880523b358e6f5140299421 (diff) | |
differentiate between concurrency enabled at command line and by git config
The latter should not affect --batch mode.
Diffstat (limited to 'Types/Concurrency.hs')
| -rw-r--r-- | Types/Concurrency.hs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Types/Concurrency.hs b/Types/Concurrency.hs index abae4a7729..ccab1ee0a9 100644 --- a/Types/Concurrency.hs +++ b/Types/Concurrency.hs @@ -17,3 +17,8 @@ parseConcurrency :: String -> Maybe Concurrency parseConcurrency "cpus" = Just ConcurrentPerCpu parseConcurrency "cpu" = Just ConcurrentPerCpu parseConcurrency s = Concurrent <$> readish s + +-- Concurrency can be configured at the command line or by git config. +data ConcurrencySetting + = ConcurrencyCmdLine Concurrency + | ConcurrencyGitConfig Concurrency |