aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorGaëtan Gilbert2021-02-04 12:14:32 +0100
committerGaëtan Gilbert2021-02-04 12:21:12 +0100
commit74aabc032014b0b83f2d54996dbb76cb5a78ea4d (patch)
tree639390a8829b8a3a91ec6361e049db1ad69f46db /plugins
parent4b7feb4e022eab13ead7468687a53bc5afae0f8f (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 'plugins')
0 files changed, 0 insertions, 0 deletions