Skip to content
Snippets Groups Projects
Commit 46f7245b authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/andre/doc-dontrun' into 'master'

[Doc] update documentation about DONTRUN

See merge request frama-c/frama-c!2741
parents 6aff333e 59587cc5
No related branches found
No related tags found
No related merge requests found
......@@ -1020,9 +1020,7 @@ directory of directory \texttt{tests}\codeidx{tests}. The
\texttt{DONTRUN} directive does not need to have any content, but it
is useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is currently developed and not fully
operational yet). If a test file is explicitly given on the command
line of \ptests, it is always executed, regardless of the presence of
a \texttt{DONTRUN} directive.
operational yet).
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment