Rename --time-mode wall-clock to --time-mode wall

This commit is contained in:
amesgen 2022-05-22 15:05:19 +02:00 committed by ˌbodʲɪˈɡrʲim
parent 114d2938f8
commit e26d65c4ca
2 changed files with 5 additions and 5 deletions

View File

@ -608,7 +608,7 @@ Use `--help` to list command-line options.
* `--time-mode`
Whether to measure CPU time ("cpu") or wall-clock time ("wall-clock") (default: cpu)
Whether to measure CPU time ("cpu") or wall-clock time ("wall") (default: cpu)
* `+RTS -T`

View File

@ -554,7 +554,7 @@ Use @--help@ to list command-line options.
[@--time-mode@]:
Whether to measure CPU time ("cpu") or wall-clock time
("wall-clock") (default: cpu)
("wall") (default: cpu)
[@+RTS@ @-T@]:
@ -818,14 +818,14 @@ instance IsOption TimeMode where
defaultValue = CpuTime
parseValue v = case v of
"cpu" -> Just CpuTime
"wall-clock" -> Just WallTime
"wall" -> Just WallTime
_ -> Nothing
optionName = pure "time-mode"
optionHelp = pure "Whether to measure CPU time (\"cpu\") or wall-clock time (\"wall-clock\")"
optionHelp = pure "Whether to measure CPU time (\"cpu\") or wall-clock time (\"wall\")"
#if MIN_VERSION_tasty(1,3,0)
showDefaultValue m = Just $ case m of
CpuTime -> "cpu"
WallTime -> "wall-clock"
WallTime -> "wall"
#endif
#endif