From 4f321fac3d4020f08aab11325654d0abd8586921 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 22 Sep 2020 09:12:53 +0200 Subject: [PATCH] [Wp/Doc] fix typo in option name --- 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 650b869af3e..3e343ef02f7 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. -- GitLab