diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-05-18 14:50:28 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-05-18 14:53:08 +0200 |
| commit | 41f0f4a53fd462cd7e0bb190ebd547409a0873de (patch) | |
| tree | de7fefb38f589e85a5d8a3578a52a8b3ccafe1b7 | |
| parent | b07c8f1224d63de6172567b04b9e008c4f18de1a (diff) | |
Adding the -color option to coqc.
coqc by default uses colors, this allows to disable it. Moreover,
colors are not yet correctly disabled when compiling from emacs (emacs
bugs?), making this option even more useful.
| -rw-r--r-- | tools/coqc.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index aed229abc..5710b97f2 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,18 +111,18 @@ let parse_args () = |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-indices-matter"|"-quick"|"-color"|"-type-in-type" + |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem (* Options for coqtop : b) options with 1 argument *) - | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" as o) :: rem -> begin match rem with |