From 74aabc032014b0b83f2d54996dbb76cb5a78ea4d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 4 Feb 2021 12:14:32 +0100
Subject: 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.
---
 test-suite/output/bug_13821_native_command_line_warn.out | 0
 test-suite/output/bug_13821_native_command_line_warn.v   | 1 +
 2 files changed, 1 insertion(+)
 create mode 100644 test-suite/output/bug_13821_native_command_line_warn.out
 create mode 100644 test-suite/output/bug_13821_native_command_line_warn.v

(limited to 'test-suite')

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
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"); -*- *)
-- 
cgit v1.2.3