aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/idetop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 8cb02190e6..a2b85041e8 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -537,5 +537,5 @@ let islave_init ~opts extra_args =
let () =
let open Coqtop in
- let custom = { init = islave_init; run = loop; } in
+ let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in
start_coq custom