aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqargs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 5b73471c5..a7065c031 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -153,7 +153,7 @@ let add_compat_require opts v =
let set_batch_mode opts =
Flags.quiet := true;
- System.trust_file_cache := false;
+ System.trust_file_cache := true;
{ opts with batch_mode = true }
let add_compile opts verbose s =