aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-07 17:52:49 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-07 17:52:49 +0200
commitd651b97b23bb827aaaf109e9bf29da244cd41704 (patch)
treec624e597a954a40de3c9a2d4d90d24870d54913b /configure.ml
parent625b08a93ffaa3d75d87861876a337666631f6e0 (diff)
parent6c4062ca13e6fb9e7d2dc93c70b545ccb22575de (diff)
Merge PR #7921: Archive the `gallina` tool
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 b264a2652..fde0a409c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -18,7 +18,7 @@ let vo_magic = 8891
let state_magic = 58891
let distributed_exec =
["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
- "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
+ "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
let verbose = ref false (* for debugging this script *)