aboutsummaryrefslogtreecommitdiff
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 113b1fb5d7..c85b656171 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -497,7 +497,7 @@ let parse_args ~help ~init arglist : t * string list =
{ oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
Stm.AsyncOpts.async_proofs_never_reopen_branch = true
}}}
- |"-test-mode" -> Vernacentries.test_mode := true; oval
+ |"-test-mode" -> Vernacinterp.test_mode := true; oval
|"-beautify" -> Flags.beautify := true; oval
|"-bt" -> Backtrace.record_backtrace true; oval
|"-color" -> set_color oval (next ())