diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index 650b869af3ec4b4989e7e1e3333dc3833c965ceb..3e343ef02f74e318d518694174ef46d0af68f881 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/src/plugins/wp/doc/manual/wp_plugin.tex @@ -1455,7 +1455,7 @@ several categories of formatters (PO stands for \emph{Proof Obligations}): can be written \verb+"%.."+ or \verb+"%{..}"+. When \verb+range+ is used instead of \verb+steps+, the maximal number $n$ of steps is printed as a range $a..b$ that contains $n$. -When option \verb+-report-json+ is used, the previous rank $a$ and $b$ are kept when +When option \verb+-wp-report-json+ is used, the previous rank $a$ and $b$ are kept when available and still fits with the new maximal step number. Otherwise, $a$ and $b$ are re-adjusted following an heurisitics designed to increase the stability for non-regression testing.