revert change - this was due to an bug in php HEAD a few days ago

diff --git a/pear/Console/Getopt.php b/pear/Console/Getopt.php
index 15fe9efe34fe389be06717c0df505893df242c88..964421943f27f70a3326d31a3de0dc84d88697f7 100644 (file)
--- a/pear/Console/Getopt.php
+++ b/pear/Console/Getopt.php
@@ -82,7 +82,6 @@ class Console_Getopt {
         }
         if (isset($args[0]{0}) && $args[0]{0} != '-') {
             array_shift($args);
-            $args = array_values($args);
         }
         reset($args);
         while (list($i, $arg) = each($args)) {