diff options
| -rwxr-xr-x | toolchain/dependencies/dependencies.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toolchain/dependencies/dependencies.sh b/toolchain/dependencies/dependencies.sh index 98a9d6f92..9e2e50b4c 100755 --- a/toolchain/dependencies/dependencies.sh +++ b/toolchain/dependencies/dependencies.sh @@ -165,8 +165,8 @@ if [ -z "$MAKE_VERSION" ] ; then fi; MAKE_MAJOR=$(echo $MAKE_VERSION | $XSED -e "s/\..*//g") MAKE_MINOR=$(echo $MAKE_VERSION | $XSED -e "s/^$MAKE_MAJOR\.//g" -e "s/\..*//g" -e "s/[a-zA-Z].*//g") -if [ $MAKE_MAJOR -lt 3 ] || [ $MAKE_MAJOR -eq 3 -a $MAKE_MINOR -lt 80 ] ; then - echo "You have make '$MAKE_VERSION' installed. GNU make >=3.80 is required" +if [ $MAKE_MAJOR -lt 3 ] || [ $MAKE_MAJOR -eq 3 -a $MAKE_MINOR -lt 81 ] ; then + echo "You have make '$MAKE_VERSION' installed. GNU make >=3.81 is required" exit 1; fi; echo "GNU make version '$MAKE_VERSION': Ok" |