diff options
author | lloyd <[email protected]> | 2011-02-18 13:32:26 +0000 |
---|---|---|
committer | lloyd <[email protected]> | 2011-02-18 13:32:26 +0000 |
commit | 8d552765fa9eb30d733909dcebd6f3f09dc4c3de (patch) | |
tree | 958702311b590f7ee86655749cda0eb7f0acbb0d | |
parent | 20b9d66dc60595e685d99f59a7ef306074d8e0b1 (diff) |
Canonicalize OS name for Cygwin; apparently platform will report
things like cygwin_nt-5.1 in some cases.
-rwxr-xr-x | configure.py | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/configure.py b/configure.py index e91dc2934..2a3e8cccd 100755 --- a/configure.py +++ b/configure.py @@ -1509,6 +1509,11 @@ def main(argv = None): if options.os is None: options.os = platform.system().lower() + + if re.match('^cygwin_.*', options.os): + logging.debug("Converting '%s' to 'cygwin'", options.os) + options.os = 'cygwin' + logging.info('Guessing taget OS is %s (--os to set)' % (options.os)) if options.compiler is None: |