diff --git a/dev/ci/user-overlays/19981-SkySkimmer-classify-warn.sh b/dev/ci/user-overlays/19981-SkySkimmer-classify-warn.sh new file mode 100644 index 000000000000..c372ae9215a4 --- /dev/null +++ b/dev/ci/user-overlays/19981-SkySkimmer-classify-warn.sh @@ -0,0 +1 @@ +overlay metacoq https://github.com/SkySkimmer/metacoq classify-warn 19981 diff --git a/doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst b/doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst new file mode 100644 index 000000000000..656fa5947343 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/19981-classify-warn.rst @@ -0,0 +1,5 @@ +- **Fixed:** + :opt:`Debug` and :opt:`Warnings` are classified as Synterp. + This changes the scheduling during :cmd:`Import` such that putting `#[export] Set Warnings` around a specific command may change behaviour. + (`#19981 `_, + by Gaƫtan Gilbert). diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 536f642473f0..a9f959d1baf2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1967,7 +1967,7 @@ let () = CWarnings.normalize_flags_string flags in declare_string_option ~preprocess - { optstage = Summary.Stage.Interp; + { optstage = Summary.Stage.Synterp; optdepr = None; optkey = ["Warnings"]; optread = CWarnings.get_flags; @@ -1975,7 +1975,7 @@ let () = let () = declare_string_option - { optstage = Summary.Stage.Interp; + { optstage = Summary.Stage.Synterp; optdepr = None; optkey = ["Debug"]; optread = CDebug.get_flags;