diff options
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 19bae4f19a..86a7ea8476 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 |