aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-15 04:15:55 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-23 19:30:17 +0100
commited09ae7a473a99c914f2af64d3387d9190e85849 (patch)
treee5b51993dc0602eb1fa985d293d82c03d286ec86 /toplevel/coqinit.ml
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff)
[flags] Move global time flag into an attribute.
One less global flag.
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3a195c1df..176dfb3c9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
let load_rc = ref true
let no_load_rc () = load_rc := false
-let load_rcfile doc sid =
+let load_rcfile ~time doc sid =
if !load_rc then
try
if !rcfile_specified then
if CUnix.file_readable_p !rcfile then
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else
try
@@ -43,7 +43,7 @@ let load_rcfile doc sid =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
with Not_found -> doc, sid
(*
Flags.if_verbose