diff options
| author |  Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 14:21:13 +0100 |
|---|---|---|
| committer | Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 14:41:26 +0100 |
| commit | c9074aa238e73bb932be67c67479b11bc95cd47a (patch) | |
| tree | 02ed451f463c8973425568f4b34bcb2772ca1984 | |
| parent | 2ef5fa7910e644d7eb39ee01024878a67086bd42 (diff) | |
add coqdep in distributed_exec, else make does not work.
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 45912615e..9ff483603 100644 --- a/configure.ml +++ b/configure.ml @@ -17,7 +17,7 @@ three non-negative, period-separed integers [...]" *) let vo_magic = 8591 let state_magic = 58501 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; -"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert"] +"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) |