diff options
| author | Théo Zimmermann | 2020-02-14 17:12:47 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-14 17:12:47 +0100 |
| commit | df94f1a5430dde7cee6ccb1c16854bcbc94575c8 (patch) | |
| tree | 53de58ca4f8a7281eecd41ee476843e3d6e59d19 /test-suite | |
| parent | 90ccf8e413aea57ec670ea26174d3deffb4036aa (diff) | |
| parent | 8d03696658e409df1349585d59dabe13dbf52ed2 (diff) | |
Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker packaging
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'test-suite')
| -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. |