aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorEnrico Tassi2014-09-01 14:54:49 +0200
committerEnrico Tassi2014-09-02 11:29:42 +0200
commitcf6b12cb3a88fb3af6a7b3e91d17db8b06d23c81 (patch)
tree46ec306afd1ebf29b735e7f6679c8e1b8d9c5679 /Makefile.common
parent7befcc7ea63ea4bd6e45e6f4b8ec01a69b586cc7 (diff)
coqworkmgr
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 5b90e19db7..44cdc0baf5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -94,8 +94,10 @@ COQTEX:=bin/coq-tex$(EXE)
COQWC:=bin/coqwc$(EXE)
COQDOC:=bin/coqdoc$(EXE)
FAKEIDE:=bin/fake_ide$(EXE)
+COQWORKMGR:=bin/coqworkmgr$(EXE)
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
+ $(COQWORKMGR)
PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT)