When a file is executed on the command line without the --file argument,
$_SERVER['argv'] contains an extraneous empty string at the beginning of
the array. (Note this bug does not occur when the --file argument is used.)
Github pull request 767: https://github.com/facebook/hiphop-php/pull/767