diff options
| -rw-r--r-- | manual/index.html | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/manual/index.html b/manual/index.html index 0193101f..93e1dced 100644 --- a/manual/index.html +++ b/manual/index.html @@ -372,9 +372,8 @@ using some command-line options:</p> <ul> <li><code>--</code>:</li> </ul> -<p>Terminates argument processing. Remaining arguments are - positional, either strings, JSON texts, or input filenames, - according to whether <code>--args</code> or <code>--jsonargs</code> were given.</p> +<p>Terminates argument processing. Remaining arguments are not + interpreted as options.</p> <ul> <li><code>--run-tests [filename]</code>:</li> </ul> |