diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/lib/system.ml b/lib/system.ml index 2c8dbac7c0..dfede29e8f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* $Id$ *) @@ -54,7 +56,8 @@ let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) -let trust_file_cache = ref true +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = @@ -294,18 +297,18 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time time f x = +let with_time ~batch f x = let tstart = get_time() in - let msg = if time then "" else "Finished transaction in " in + let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in - let msg2 = if time then "" else " (successful)" in + let msg2 = if batch then "" else " (successful)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in - let msg = if time then "" else "Finished failing transaction in " in - let msg2 = if time then "" else " (failure)" in + let msg = if batch then "" else "Finished failing transaction in " in + let msg2 = if batch then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e |