From 8e1ef081278c738d5f8cf3dc26d19a8fdf05862e Mon Sep 17 00:00:00 2001 From: cdeler Date: Sat, 8 Dec 2018 21:18:53 +0300 Subject: [PATCH] Fixup the issue related with an incorrect distro version string handling --- python/servo/bootstrap.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/python/servo/bootstrap.py b/python/servo/bootstrap.py index 4f3f84ebcae..4f9744a7c17 100644 --- a/python/servo/bootstrap.py +++ b/python/servo/bootstrap.py @@ -345,7 +345,10 @@ def get_linux_distribution(): distro, version, _ = platform.linux_distribution() if distro == 'LinuxMint': - major, minor = version.split('.') + if '.' in version: + major, _ = version.split('.', 1) + else: + major = version if major == '19': base_version = '18.04'