aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:21:19 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-11-22 14:21:19 +0100
commitcf646d855395a9d0c40613098debbbd895c4eef8 (patch)
tree1210165fb6472623dbabc6e5afe365fdd38ad205 /configure
parent6fb31c8a00e67f5a91983fe92f6df95d5f54a0c1 (diff)
downloadcompcert-cf646d855395a9d0c40613098debbbd895c4eef8.tar.gz
compcert-cf646d855395a9d0c40613098debbbd895c4eef8.zip
Replace ocamlbuild by a second-stage makefile to compile the OCaml code and produce the executables.
configure: add check for GNU make.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure18
1 files changed, 18 insertions, 0 deletions
diff --git a/configure b/configure
index fda59dab..f3967dc7 100755
--- a/configure
+++ b/configure
@@ -253,6 +253,23 @@ case "$menhir_ver" in
missingtools=true;;
esac
+echo "Testing GNU make..." | tr -d '\n'
+make=''
+for mk in make gmake gnumake; do
+ make_ver=`$mk -v | head -1 | sed -n -e 's/^GNU Make //p'`
+ case "$make_ver" in
+ 3.8*|3.9*|[4-9].*)
+ echo "version $make_ver (command '$mk') -- good!"
+ make="$mk"
+ break;;
+ esac
+done
+if test -z "$make"; then
+ echo "NOT FOUND"
+ echo "Error: make sure GNU Make version 3.80 or later is installed."
+ missingtools=true
+fi
+
if $missingtools; then
echo "One or several required tools are missing or too old. Aborting."
exit 2
@@ -403,6 +420,7 @@ CompCert configuration:
Runtime library provided...... $has_runtime_lib
Library files installed in.... $libdirexp
cchecklink tool supported..... $cchecklink
+ Build command to use.......... $make
If anything above looks wrong, please edit file ./Makefile.config to correct.