aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
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 /configure.ml
parent0be49a49c41e28b2015440723882e0ca15c02d5e (diff)
parent103f59ed6b8174ed9359cb11c909f1b2219390c9 (diff)
Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.
Reviewed-by: maximedenes Ack-by: ppedrot
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 6f5ade3b9a..ef38651a4d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -19,7 +19,7 @@ let vo_magic = 8991
let state_magic = 58991
let distributed_exec =
["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
- "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
+ "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
let verbose = ref false (* for debugging this script *)