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`.
---
 lib/aux_file.mli | 2 +-
 lib/flags.ml     | 2 --
 lib/flags.mli    | 4 ----
 3 files changed, 1 insertion(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 60c8fb4449..b241fdc6cc 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t
 
 val aux_file_name_for : string -> string
 val start_aux_file : aux_file:string -> v_file:string -> unit
-val stop_aux_file : unit -> unit 
+val stop_aux_file : unit -> unit
 val recording : unit -> bool
 
 val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index 190de5853d..f09dc48f5d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -41,8 +41,6 @@ let with_options ol f x =
     let () = List.iter2 (:=) ol vl in
     Exninfo.iraise reraise
 
-let record_aux_file = ref false
-
 let async_proofs_worker_id = ref "master"
 let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 1c96796220..185a5f8425 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -31,10 +31,6 @@
 
 (** Command-line flags  *)
 
-(** Set by coqtop to tell the kernel to output to the aux file; will
-    be eventually removed by cleanups such as PR#1103 *)
-val record_aux_file : bool ref
-
 (** Async-related flags *)
 val async_proofs_worker_id : string ref
 val async_proofs_is_worker : unit -> bool
-- 
cgit v1.2.3