diff --git a/prelude.sh b/prelude.sh index b90ce75b9..e38694b7d 100644 --- a/prelude.sh +++ b/prelude.sh @@ -77,7 +77,6 @@ if [[ "${__INITPC_PRELUDE_SOURCED__}" != "true" ]]; then fi } - # TODO make distro_version_le # @param $1 - minimal distro major version function distro_version_ge { @@ -92,6 +91,7 @@ if [[ "${__INITPC_PRELUDE_SOURCED__}" != "true" ]]; then VERSION_ID="$(source /etc/os-release && echo "${VERSION_ID}")" echo "Version ID=${VERSION_ID}" + # An empty VERSION_ID is interpretted as the (positive) infinity. if [[ ${VERSION_ID} == "" ]]; then echo "Warning: The version ID is empty." return @@ -106,6 +106,16 @@ if [[ "${__INITPC_PRELUDE_SOURCED__}" != "true" ]]; then fi } + function distro_version_lt { + $(distro_version_ge "$1") + if [[ $? == ${EXIT_INCORRECT_PLATFORM} ]]; then + return + else + # If VERSION_ID is empty we fail. + exit ${EXIT_INCORRECT_PLATFORM} + fi + } + function gnome_present { local GNOME_PRESENT="no"