mirror of
https://github.com/servo/servo.git
synced 2025-07-02 13:03:43 +01:00
Fixup the issue related with an incorrect distro version string handling
This commit is contained in:
parent
8fb1b567fa
commit
8e1ef08127
1 changed files with 4 additions and 1 deletions
|
@ -345,7 +345,10 @@ def get_linux_distribution():
|
||||||
distro, version, _ = platform.linux_distribution()
|
distro, version, _ = platform.linux_distribution()
|
||||||
|
|
||||||
if distro == 'LinuxMint':
|
if distro == 'LinuxMint':
|
||||||
major, minor = version.split('.')
|
if '.' in version:
|
||||||
|
major, _ = version.split('.', 1)
|
||||||
|
else:
|
||||||
|
major = version
|
||||||
|
|
||||||
if major == '19':
|
if major == '19':
|
||||||
base_version = '18.04'
|
base_version = '18.04'
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue