idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-16 15:52:43 +03:00
Code Issues Projects Releases Wiki Activity

rename experimental command line flag and group with the other experimental feature.

Browse Source
This commit is contained in:
Mathew Polzin 2021-07-15 17:24:12 -07:00
parent 89125e96dd
commit ec3b868cb6
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/CommandLine.idr
View File

@ -234,8 +234,6 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just $ "Set output directory"),
MkOpt ["--profile"] [] [Profile]
(Just "Generate profile data when compiling, if supported"),
MkOpt ["--case-tree-opt"] [] [CaseTreeHeuristics]
(Just "Apply experimental optimizations to case tree generation"),
optSeparator,
MkOpt ["-Werror"] [] [WarningsAsErrors]
@ -246,6 +244,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
optSeparator,
MkOpt ["-Xcheck-hashes"] [] [HashesInsteadOfModTime]
(Just "Use SHA256 hashes instead of modification time to determine if a source file needs rebuilding"),
MkOpt ["-Xcase-tree-opt"] [] [CaseTreeHeuristics]
(Just "Apply experimental optimizations to case tree generation"),
optSeparator,
MkOpt ["--prefix"] [] [ShowPrefix]