From 6c06f36b2dd1812454d40cbde1da28e1ea8be67e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 13:34:02 +0100
Subject: Make boot flag into a normal option (no global flag).

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

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 7336b9beaf..607f0e2e49 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -31,8 +31,6 @@
 
 (** Command-line flags  *)
 
-val boot : bool ref
-
 (** 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
-- 
cgit v1.2.3