From ed09ae7a473a99c914f2af64d3387d9190e85849 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 Dec 2017 04:15:55 +0100
Subject: [flags] Move global time flag into an attribute.

One less global flag.
---
 lib/flags.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 000862b2c6..62328e3d34 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,9 +35,6 @@ val profile : bool
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
-(* -time option: every command will be wrapped with `Time` *)
-val time : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
-- 
cgit v1.2.3