aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-12-25 15:39:42 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-12-25 15:39:42 +0100
commita138b43ccb391be63bed2fea26cd36dab96b091f (patch)
tree5c88028afca1db1c3e70299797fe33a261039cad /configure
parent2a9a34bc137b1ba81ab4f6e90a447ae9d64e344b (diff)
downloadcompcert-kvx-a138b43ccb391be63bed2fea26cd36dab96b091f.tar.gz
compcert-kvx-a138b43ccb391be63bed2fea26cd36dab96b091f.zip
configure: use `$make` instead of `make`
To make sure it works if `gmake` is required. Fixes: #381
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index c5afabd8..0ca893d2 100755
--- a/configure
+++ b/configure
@@ -768,7 +768,7 @@ B cparser
B extraction
EOF
-make CoqProject
+$make CoqProject
#
# Clean up target-dependent files to force their recompilation