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.
---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 24a99d57f6..892c05b64d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4294,7 +4294,7 @@ sig
 type vernac_control =
   | VernacExpr of vernac_expr
    (* Control *)
-  | VernacTime of vernac_control Loc.located
+  | VernacTime of bool * vernac_control Loc.located
   | VernacRedirect of string * vernac_control Loc.located
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
-- 
cgit v1.2.3