aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-02 14:33:02 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-02 14:38:39 +0200
commit4648732544f43ad87266f33967995b29d2b8338b (patch)
treefb2adf37e3c008dd4af4141d402dbefe62074139 /Makefile.common
parent134fb9534d3e9dd4b20721f9c04fee7db217e883 (diff)
Makefile.common: update PRIVATEBINARIES to repair the build on MACOS
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 19bae4f19..86a7ea847 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -98,7 +98,7 @@ COQWORKMGR:=bin/coqworkmgr$(EXE)
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
$(COQWORKMGR)
-PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP)
+PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT)
###########################################################################
# Documentation