diff options
| author | Enrico Tassi | 2015-05-28 19:00:07 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-05-29 15:44:47 +0200 |
| commit | f63c0cdd3c7da642e505569e83199784bbfdc367 (patch) | |
| tree | 6556a9e2f016d56cb70849c5ef75a9a545f95527 /kernel | |
| parent | c47916933025a4853ed0b397d7476b844bb894a4 (diff) | |
make Unset Silent work in coqc
Trying to untangle the flags:
coqc -verbose coqtop -compile-verbose are used just to print the commands run;
-quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag.
Flags.verbose controls many prints that are expected to be made in
interactive mode. E.g. "Proof" or "tac" prints goals if such flag is
true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc
mode.
It is still messy, but the confusion between -verbose and Flags.verbose
has gone (I must have identified the two things with my initial STM
patch)
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
