diff options
| author | Hugo Herbelin | 2020-08-24 16:40:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-24 16:40:58 +0200 |
| commit | d49b9f298e46df177400cae775a1c22879543456 (patch) | |
| tree | 21ea97ea49656ae39807d0d2eea1f6629ab0b0d8 /test-suite/Makefile | |
| parent | 188e8f7084b586f2e555a5770d24eec8ebd05d91 (diff) | |
| parent | 81ed30792484b5fb947b8e53f1363574015ce546 (diff) | |
Merge PR #12835: Slightly reorganising the test suite to follow its documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 28add48b36..5d4e15b985 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -222,7 +222,7 @@ report: summary.log # printed for all opened bugs (still active or seems to be closed). # For closed bugs that behave as expected, no message is printed -# All files are assumed to have <# of the bug>.v as a name +# All files are assumed to have bug_<# of the bug>.v as a name # Opened bugs that should not fail $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v |