Skip to content

Commit 125ecbc

Browse files
committed
fix test-suite rocq 9
1 parent 8692b08 commit 125ecbc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Makefile.test-suite.coq.local

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ output_for=`\
99
DIFF=\
1010
@if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
1111
echo OUTPUT DIFF $(1);\
12-
$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
12+
$(COQTOP) $(COQFLAGS) $(COQLIBS) -w -deprecated-from-Coq -topfile $(1) \
1313
< $(1) 2>&1 \
1414
| sed 's/Coq < *//g' \
1515
| sed 's/Rocq < *//g' \

0 commit comments

Comments
 (0)