diff --git a/tools/make_disc_trees.pl b/tools/make_disc_trees.pl index ca3a7988..531048a2 100755 --- a/tools/make_disc_trees.pl +++ b/tools/make_disc_trees.pl @@ -1082,6 +1082,7 @@ sub add_trans_desc_entry { # so, we'll need to uncompress again on entry here. if (-f "$trans_file.gz") { + system("rm -f $trans_file"); system("gunzip $trans_file.gz"); } @@ -1253,6 +1254,7 @@ sub remove_trans_desc_entry { # Keeping files in .gz format is expensive - see comment # in add_trans_desc_entry() above. if (-f "$trans_file.gz") { + system("rm -f $trans_file"); system("gunzip $trans_file.gz"); } $st = stat("$trans_file") || die "unable to stat $trans_file\n";