diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-18 14:32:22 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-18 14:32:22 +0100 |
| commit | c8287e6578f313769c794fd407868b1ecb51c43f (patch) | |
| tree | 4536804562f316d3bcf75ee1e38e33b98afcd08a /configure | |
| parent | e11388aac1f4f635e3c32d9b3200de16d779c630 (diff) | |
| download | compcert-c8287e6578f313769c794fd407868b1ecb51c43f.tar.gz compcert-c8287e6578f313769c794fd407868b1ecb51c43f.zip | |
One more cleanup in configure.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -272,7 +272,7 @@ esac echo "Testing GNU make... " | tr -d '\n' make='' for mk in make gmake gnumake; do - make_ver=`($mk -v 2>/dev/null | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null` + make_ver=`$mk -v 2>/dev/null | 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!" |