From 6c1add07712d7823526bafc62a808ceca231bf6e Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 4 Oct 2023 05:04:08 +0000
Subject: Update website

---
 manual/index.html | 5 ++---
 1 file 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>
-- 
cgit v1.2.3