diff options
| -rwxr-xr-x | scripts/dev/gen_stub.php | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/scripts/dev/gen_stub.php b/scripts/dev/gen_stub.php index 993be075d7..f61893050c 100755 --- a/scripts/dev/gen_stub.php +++ b/scripts/dev/gen_stub.php @@ -384,8 +384,12 @@ function initPhpParser() { if (!is_dir($phpParserDir)) { $cwd = getcwd(); chdir(__DIR__); + passthru("wget https://github.com/nikic/PHP-Parser/archive/v$version.tar.gz", $exit); if ($exit !== 0) { + passthru("curl -LO https://github.com/nikic/PHP-Parser/archive/v$version.tar.gz", $exit); + } + if ($exit !== 0) { throw new Exception("Failed to download PHP-Parser tarball"); } if (!mkdir($phpParserDir)) { |