Skip to content

Commit 080f565

Browse files
committed
Make argument-scope-delimiter error by default
In order to actually handle this 8.19 deprecation in 9.4.
1 parent 93c35c9 commit 080f565

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

vernac/comArguments.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ let warn_arguments_assert =
5959

6060
let warn_scope_delimiter_depth =
6161
CWarnings.create ~name:"argument-scope-delimiter" ~category:Deprecation.Version.v8_19
62+
~default:AsError
6263
Pp.(fun () ->
6364
strbrk "The '%' scope delimiter in 'Arguments' commands is deprecated, " ++
6465
strbrk "use '%_' instead (available since 8.19). The '%' syntax will be " ++

0 commit comments

Comments
 (0)