diff options
| author | github-actions[bot] <github-actions[bot]@users.noreply.github.com> | 2023-10-04 05:04:08 +0000 |
|---|---|---|
| committer | github-actions[bot] <github-actions[bot]@users.noreply.github.com> | 2023-10-04 05:04:08 +0000 |
| commit | 6c1add07712d7823526bafc62a808ceca231bf6e (patch) | |
| tree | ea6218ba747e7454291e56cf6ff5da923da7795e | |
| parent | 791f9c641740e746c8c19c26bdf7fdc46a64e978 (diff) | |
Update website
| -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> |