diff options
| author | Emilio Jesus Gallego Arias | 2019-08-08 23:15:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-26 11:45:45 +0200 |
| commit | 61f4df8b5b974302e8b48bcf271aa68757db69fe (patch) | |
| tree | dd9ba4f3f07045f06f8594f65184280a90d43ab8 /stm/vio_checking.ml | |
| parent | 09953295ea86eaf78c6688a1a2861aa6f41cd9ab (diff) | |
[glob/aux files] Remove undocumented Stdout dump, cleanup flags.
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
Diffstat (limited to 'stm/vio_checking.ml')
| -rw-r--r-- | stm/vio_checking.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - |