diff options
-rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -55,6 +55,7 @@ tools: # The following PHONY rule is important for Cygwin: .PHONY: install install: + mkdir -p $(DESTDIR) $(OCAMLFIND_DESTDIR) $(OCAMLFIND_DESTDIR)/stublibs for pkg in $(PKGLIST); do \ ( cd src/$$pkg && $(MAKE) -f Makefile.pre install ) || exit; \ done |