diff options
author | David Allsopp <david.allsopp@metastack.com> | 2019-10-15 11:46:36 +0100 |
---|---|---|
committer | David Allsopp <david.allsopp@metastack.com> | 2019-10-15 11:46:36 +0100 |
commit | 13786d7d1227df99724214051d0d5c40028f8003 (patch) | |
tree | a6df6af82268f890d94db30b5d2e3b7f382c4afd /otherlibs/Makefile | |
parent | cc6c09edbee3038ed8ffa2ee1bb0081bf177cc1f (diff) | |
download | ocaml-13786d7d1227df99724214051d0d5c40028f8003.tar.gz |
Ensure make distclean works on an unconfigured tree
Diffstat (limited to 'otherlibs/Makefile')
-rw-r--r-- | otherlibs/Makefile | 3 |
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: |