diff options
| author | Erik Martin-Dorel | 2020-01-28 02:32:41 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2020-01-28 22:46:50 +0100 |
| commit | 654326961d151dfff62a58aef8f16a00ed39b6b8 (patch) | |
| tree | 307b141a2bca05b2f0745edafefcbf3a256004b3 | |
| parent | 861e3ed8b0c96354c959767ae4750e28193f8d38 (diff) | |
docs: Add missing prefix (bug_*.v)
Related: https://github.com/coq/coq/pull/8630
| -rw-r--r-- | test-suite/README.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/README.md b/test-suite/README.md index a2d5905710..96926f70b9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information. ## Adding a test Regression tests for closed bugs should be added to -[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number. +[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well. |