diff --git a/tools/update_versions b/tools/update_versions
index 3a8a0e8d44..5249f0346c 100755
--- a/tools/update_versions
+++ b/tools/update_versions
@@ -89,6 +89,7 @@ function file_info_xml($fd) {
if (is_array($fd->url)) {
foreach ($fd->url as $url) {
$xml .= " $url\n";
+ $xml .= " $url.gz\n";
}
} else {
$xml .= " $fd->url\n";
@@ -170,7 +171,9 @@ function stage_file($a, $v, $p, $fd) {
system("cp $path $dl_path");
}
- $fd->url = "$download_url/$name";
+ if (!sizeof($fd->url)) {
+ $fd->url = "$download_url/$name";
+ }
if ($fd->gzip) {
if (!file_exists("$dl_path.gz")) {
$tmp = "$dl_path.tmp";
@@ -256,9 +259,7 @@ function process_file($a, $v, $p, $name, $fds) {
}
}
- if (!sizeof($fd->url)) {
- $fd = stage_file($a, $v, $p, $fd);
- }
+ $fd = stage_file($a, $v, $p, $fd);
if (!isset($fd->executable)) {
$perms = fileperms($path);