diff --git a/BuildLinux.sh b/BuildLinux.sh index abb81ca737..28d84fb046 100755 --- a/BuildLinux.sh +++ b/BuildLinux.sh @@ -80,7 +80,7 @@ fi DISTRIBUTION=$(awk -F= '/^ID=/ {print $2}' /etc/os-release) # treat ubuntu as debian -if [ "${DISTRIBUTION}" == "ubuntu" ] +if [ "${DISTRIBUTION}" == "ubuntu" ] || [ "${DISTRIBUTION}" == "linuxmint" ] then DISTRIBUTION="debian" fi