From c9074aa238e73bb932be67c67479b11bc95cd47a Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire
Date: Thu, 26 Mar 2015 14:21:13 +0100
Subject: add coqdep in distributed_exec, else make does not work.

---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 45912615e2..9ff483603c 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 *)
 
-- 
cgit v1.2.3