From 61f4df8b5b974302e8b48bcf271aa68757db69fe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 8 Aug 2019 23:15:19 +0200
Subject: [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`.
---
 stm/vio_checking.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'stm')

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
-
-  
-- 
cgit v1.2.3