diff options
| author | Pierre Courtieu | 2015-05-18 14:50:28 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2015-05-18 14:53:08 +0200 |
| commit | 41f0f4a53fd462cd7e0bb190ebd547409a0873de (patch) | |
| tree | de7fefb38f589e85a5d8a3578a52a8b3ccafe1b7 /lib | |
| 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.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions