diff options
| author | Daniel Neus <[email protected]> | 2016-07-14 12:17:57 +0200 |
|---|---|---|
| committer | Daniel Neus <[email protected]> | 2016-07-14 14:01:44 +0200 |
| commit | 3572799ea8e53342778fcf476a15e330922ca279 (patch) | |
| tree | 73156180e5f70dcdddb1e768b30b8d2f715290e2 /configure.py | |
| parent | b3bc80dfdb28aee0900b6ed92dff5ba8c5e4daf9 (diff) | |
coverage should be checked without optimizations
Diffstat (limited to 'configure.py')
| -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 [] |