diff options
| author | Enrico Tassi | 2016-09-30 10:14:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-30 10:54:42 +0200 |
| commit | 775b8f28562d1d5063da2b28a06e59610b76f06f (patch) | |
| tree | f8360212d2dabfbae2ebe06aa5d7b40cc3247992 | |
| parent | 61112fa8bd336b17f4a2e724c4751c550f27c69a (diff) | |
Ignore file names in warning emitted by test-suite/output/* (#5111)
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 18 |
2 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae4..6ecc7bcaad 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -280,7 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ - | grep -v "^<W>" \ + | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 815305581c..1633ad9765 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,20 @@ -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +[arguments-ignore-rename-nonimpl,vernacular] +File "stdin", line 2, characters 0-25: Warning: This command is just asserting the number and names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' [arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +File "stdin", line 4, characters 0-40: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -121,9 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. |