diff options
author | Jack Lloyd <[email protected]> | 2016-07-17 11:03:20 -0400 |
---|---|---|
committer | Jack Lloyd <[email protected]> | 2016-07-17 11:03:20 -0400 |
commit | 3b05092665a05a9ba887b14acbbd136caca1de77 (patch) | |
tree | e7caed96f952b2a134159a5fb27fe802a54a0ce8 | |
parent | 014bc872f824950d7d8ee6258e432605b2eb02df (diff) | |
parent | 3572799ea8e53342778fcf476a15e330922ca279 (diff) |
Merge GH #536 Disable optimizations when doing a coverage build
-rwxr-xr-x | configure.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/configure.py b/configure.py index 094768b0b..c3c4d8832 100755 --- a/configure.py +++ b/configure.py @@ -461,6 +461,9 @@ def process_command_line(args): options.no_optimizations = True options.with_debug_info = True + if options.with_coverage: + options.no_optimizations = True + def parse_multiple_enable(modules): if modules is None: return [] |