diff --git a/build-scripts/detect-environment b/build-scripts/detect-environment index 5aba2845c..6b3a14e68 100644 --- a/build-scripts/detect-environment +++ b/build-scripts/detect-environment @@ -116,12 +116,11 @@ detect_distribution() "Red Hat Enterprise Linux Server release "*) VER=${REL#Red Hat Enterprise Linux Server release } VER=${VER% \(*}; - case "$VER" in - [0-9].[0-9]);; - *) + if ! echo "$VER" | egrep '^[0-9]+.[0-9]+$' > /dev/null + then echo "Unknown RHEL Server version: $VER" - exit 42;; - esac + exit 42 + fi OS=rhel OS_VERSION="$VER" @@ -130,12 +129,11 @@ detect_distribution() "Red Hat Enterprise Linux release "*) VER=${REL#Red Hat Enterprise Linux release } VER=${VER% \(*}; - case "$VER" in - [0-9].[0-9]);; - *) + if ! echo "$VER" | egrep '^[0-9]+.[0-9]+$' > /dev/null + then echo "Unknown RHEL Server version: $VER" - exit 42;; - esac + exit 42 + fi OS=rhel OS_VERSION="$VER"