From f13a56cad95dae05b63b735fd6eb6bd4596f9a00 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 13:39:26 +0100
Subject: Move test_mode from Flags to Vernacentries (use point)

---
 lib/flags.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 2b4446a1db..bf8846417b 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,10 +35,6 @@
     be eventually removed by cleanups such as PR#1103 *)
 val record_aux_file : bool ref
 
-(* Flag set when the test-suite is called. Its only effect to display
-   verbose information for `Fail` *)
-val test_mode : bool ref
-
 (** Async-related flags *)
 val async_proofs_worker_id : string ref
 val async_proofs_is_worker : unit -> bool
-- 
cgit v1.2.3