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.
---
 intf/vernacexpr.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index a90e5501a5..5106e513b9 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -479,8 +479,9 @@ and vernac_argument_status = {
 
 type vernac_control =
   | VernacExpr of vernac_expr
-   (* Control *)
-  | VernacTime of vernac_control located
+  (* boolean is true when the `-time` batch-mode command line flag was set.
+     the flag is used to print differently in `-time` vs `Time foo` *)
+  | VernacTime of bool * vernac_control located
   | VernacRedirect of string * vernac_control located
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
-- 
cgit v1.2.3