summaryrefslogtreecommitdiff
path: root/otherlibs/Makefile
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2018-12-04 10:28:36 +0000
committerDavid Allsopp <david.allsopp@metastack.com>2018-12-04 10:28:36 +0000
commitd4a566573fa6cfc853ff25921d8d85a6a9d9e47e (patch)
treec806e0d9af929f4973c527010f12bba3f0dc97fc /otherlibs/Makefile
parent67ada54ce36e9d52cf8332285d2b6e2118ebf998 (diff)
downloadocaml-d4a566573fa6cfc853ff25921d8d85a6a9d9e47e.tar.gz
Allow make to be invoked before configure
This should be improved to give better warnings for when Makefile.config and Makefile.common are required.
Diffstat (limited to 'otherlibs/Makefile')
-rw-r--r--otherlibs/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/otherlibs/Makefile b/otherlibs/Makefile
index cc77536ba5..4c0a576849 100644
--- a/otherlibs/Makefile
+++ b/otherlibs/Makefile
@@ -14,8 +14,8 @@
#**************************************************************************
ROOTDIR=..
-include $(ROOTDIR)/Makefile.config
-include $(ROOTDIR)/Makefile.common
+-include $(ROOTDIR)/Makefile.config
+-include $(ROOTDIR)/Makefile.common
# $1: target name to dispatch to all otherlibs/*/Makefile
define dispatch_