summaryrefslogtreecommitdiff
path: root/otherlibs/Makefile
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2019-10-15 11:46:36 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2019-10-15 11:46:36 +0100
commit13786d7d1227df99724214051d0d5c40028f8003 (patch)
treea6df6af82268f890d94db30b5d2e3b7f382c4afd /otherlibs/Makefile
parentcc6c09edbee3038ed8ffa2ee1bb0081bf177cc1f (diff)
downloadocaml-13786d7d1227df99724214051d0d5c40028f8003.tar.gz
Ensure make distclean works on an unconfigured tree
Diffstat (limited to 'otherlibs/Makefile')
-rw-r--r--otherlibs/Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/otherlibs/Makefile b/otherlibs/Makefile
index 4c0a576849..8342b40251 100644
--- a/otherlibs/Makefile
+++ b/otherlibs/Makefile
@@ -17,6 +17,9 @@ ROOTDIR=..
-include $(ROOTDIR)/Makefile.config
-include $(ROOTDIR)/Makefile.common
+OTHERLIBRARIES ?= bigarray dynlink raw_spacetime_lib str systhreads \
+ unix win32unix
+
# $1: target name to dispatch to all otherlibs/*/Makefile
define dispatch_
$1: