git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3699 from jfdm/allow-highlight

Allowed `--highlight` in pkg commands.

commit674c2141797b447bfcafd497b927637dacdb7ec3 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateThu 23 Mar 2017, 11:59 (10 years ago) parent95d226fe64d8f0
2 files changed+3
compare with master
unifiedsplit
src/Idris/Package.hs+2 test/pkg001/expected+1
src/Idris/Package.hs+2
@@ -499,6 +499,7 @@ mergeOptions copts popts =
499499 chkOpt o@(UseCodegen _) = Right o
500500 chkOpt o@(Verbose _) = Right o
501501 chkOpt o@(AuditIPkg) = Right o
502+ chkOpt o@(DumpHighlights) = Right o
502503 chkOpt o = Left (unwords ["\t", show o, "\n"])
503504
504505 genErrMsg :: [String] -> String
@@ -508,6 +509,7 @@ mergeOptions copts popts =
508509 , "\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"
509510 , "\t--ibcsubdir <path>, -i --idrispath <path>"
510511 , "\t--logging-categories <cats>"
512+ , "\t--highlight"
511513 , "\nThe options need removing are:"
512514 , unlines es
513515 ]
test/pkg001/expected+1
@@ -4,6 +4,7 @@ The only changeable options are:
44 --log <lvl>, --total, --warnpartial, --warnreach, --warnipkg
55 --ibcsubdir <path>, -i --idrispath <path>
66 --logging-categories <cats>
7+ --highlight
78
89The options need removing are:
910 Quiet