aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorMaxime Dénès2019-02-04 13:05:00 +0100
committerMaxime Dénès2019-02-04 13:05:00 +0100
commit129d47518ae950c6ef1b69763e93cd70c14863f6 (patch)
treee5ae9646636c50f07c3b60e08eccb76e5b6eff96 /ide
parent0be49a49c41e28b2015440723882e0ca15c02d5e (diff)
parent103f59ed6b8174ed9359cb11c909f1b2219390c9 (diff)
Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.
Reviewed-by: maximedenes Ack-by: ppedrot
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 205f4455a3..e157696294 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -546,5 +546,5 @@ let islave_init ~opts extra_args =
let () =
let open Coqtop in
- let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in
+ let custom = { init = islave_init; run = loop; opts = Coqargs.default } in
start_coq custom