Skip to content

Commit 91c7e81

Browse files
committed
Include a reference to test tags in our documentation
regression/README.md describes the tags, but wasn't referenced from anywhere.
1 parent a36de69 commit 91c7e81

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

doc/architectural/compilation-and-development.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,12 @@ CI, should succeed), `THOROUGH` (takes too long to be run in CI, should
7777
succeed), `FUTURE` (will succeed when a planned feature is added) or
7878
`KNOWNBUG` (will succeed when a bug is fixed).
7979

80+
Test descriptions may also include a number of tags. `test.pl -I<tag>` will only
81+
run tests with a particular `<tag>`, and `test.pl -X<tag>` will run all tests
82+
except for those with a particular `<tag>`. See
83+
[regression/README.md](https://github.com/diffblue/cbmc/blob/develop/regression/README.md)
84+
for the current set of tags and their intended use.
85+
8086
\subsubsection compilation-and-development-subsubsection-running-regression-tests-with-make Running regression tests with make
8187

8288
If you have compiled using `make` then you can run the regression tests

0 commit comments

Comments
 (0)