Silence warning in test (#18)

SkySkimmer · Dec 4, 2023 · 9f6ed69 · 9f6ed69
2 parents 886c17f + a78c3f9
commit 9f6ed69
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/tests/compiler_bug_14.v b/tests/compiler_bug_14.v
@@ -4,6 +4,10 @@ Ltac2 test () := match mut with () => () end.
 
 From Ltac2Compiler Require Import Ltac2Compiler.
 
+Set Warnings "+tac2compile-skipped-mutable".
+Fail Ltac2 Compile test.
+
+Set Warnings "-tac2compile-skipped-mutable".
 Ltac2 Compile test.
 (*
 Dynlink error: execution of module initializers in the shared library failed: