From ca5b8000fd9d84c17201b9d37762510d450fa8fa Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 5 Mar 2019 10:17:09 +0100
Subject: [PATCH] [wp/manual] The selection of check assertions complies with
option -wp-prop.
---
src/plugins/wp/doc/manual/wp_plugin.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 6d1d1a3a70c..40d9d63d4db 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -754,7 +754,7 @@ interface of the programmatic API.
\texttt{@<category>} of properties.
\\
Recognized categories are: \texttt{@lemma}, \texttt{@requires}, \texttt{@assigns},
- \texttt{@ensures}, \texttt{@exits}, \texttt{@assert},
+ \texttt{@ensures}, \texttt{@exits}, \texttt{@assert}, \texttt{@check},
\texttt{@invariant}, \texttt{@variant}, \texttt{@breaks},
\texttt{@continues}, \texttt{@returns}, \\
\texttt{\mbox{@complete\_behaviors}}, \texttt{\mbox{@disjoint\_behaviors}}.
--
GitLab