diff options
| author | Gaëtan Gilbert | 2021-02-04 12:14:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-04 12:21:12 +0100 |
| commit | 74aabc032014b0b83f2d54996dbb76cb5a78ea4d (patch) | |
| tree | 639390a8829b8a3a91ec6361e049db1ad69f46db /test-suite | |
| parent | 4b7feb4e022eab13ead7468687a53bc5afae0f8f (diff) | |
Properly handle ordering of -w and -native-compiler
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_13821_native_command_line_warn.out | 0 | ||||
| -rw-r--r-- | test-suite/output/bug_13821_native_command_line_warn.v | 1 |
2 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.out diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v new file mode 100644 index 0000000000..a28210b6c2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *) |