--- php/generator/generator.php.orig	Thu Jul  3 13:12:27 2003
+++ php/generator/generator.php	Thu Jul  3 13:10:39 2003
@@ -732,6 +732,7 @@
 $argc = $HTTP_SERVER_VARS['argc'];
 $argv = $HTTP_SERVER_VARS['argv'];
 
+foreach($argv as $k=>$v) if ($v=="--") unset($argv[$k]);
 /* An ugly hack to counteract PHP's pernicious desire to treat + as an argument
    separator in command-line version. */
 array_walk($argv, create_function('&$x', '$x = urldecode($x);'));