diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-02 14:33:02 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-02 14:38:39 +0200 |
commit | 4648732544f43ad87266f33967995b29d2b8338b (patch) | |
tree | fb2adf37e3c008dd4af4141d402dbefe62074139 /Makefile.common | |
parent | 134fb9534d3e9dd4b20721f9c04fee7db217e883 (diff) |
Makefile.common: update PRIVATEBINARIES to repair the build on MACOS
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 2 |
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 |