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/flags.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'lib/flags.ml')

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