summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index f0c33a01..3f31036b 100644
--- a/Makefile
+++ b/Makefile
@@ -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