diff --git a/modules/base/pymod/settings.py b/modules/base/pymod/settings.py index 56bf46b4aeedf36cfcd471390cf361860608682e..34afdc0b2c9bd0db42619ab898b83a544dc48d7f 100644 --- a/modules/base/pymod/settings.py +++ b/modules/base/pymod/settings.py @@ -1,6 +1,18 @@ import os, platform import __main__ +def GetPlatform(): + """ + Returns platform.system(). If the system call is interrupted, it is repeated. + This function is a workaround for the buggy system call handling in Python. + """ + system=None + while not system: + try: + system=platform.system() + except IOError: + pass + return system def GetValue(val_key,val_default=None,prefix='OST'): """ @@ -89,7 +101,7 @@ def Locate(file_name, explicit_file_name=None, search_paths=[], if search_system_paths: paths=os.getenv('PATH') - if platform.system() == "Windows": + if GetPlatform() == "Windows": searched+=paths.split(';') else: searched+=paths.split(':')