Index: tools/coverity/coverity.py |
=================================================================== |
--- tools/coverity/coverity.py (revision 89310) |
+++ tools/coverity/coverity.py (working copy) |
@@ -135,7 +135,7 @@ |
print 'Elapsed time: %ds' % (time.time() - start_time) |
# Do a clean build. Remove the build output directory first. |
- if sys.platform == 'linux2': |
+ if sys.platform.startswith('linux'): |
rm_path = os.path.join(options.source_dir,'src','out',options.target) |
elif sys.platform == 'win32': |
rm_path = os.path.join(options.source_dir,options.solution_dir, |
@@ -165,7 +165,7 @@ |
print 'Elapsed time: %ds' % (time.time() - start_time) |
use_shell_during_make = False |
- if sys.platform == 'linux2': |
+ if sys.platform.startswith('linux'): |
use_shell_during_make = True |
os.chdir('src') |
_RunCommand('pwd', options.dry_run, shell=True) |