# HG changeset patch
# User wenzelm
# Date 1343391304 -7200
# Node ID cc7990d6eb38e85f79ef0faf04fb252d655158ae
# Parent  49afe0e921630129212dbabfbaba7754d64acb5c
delete other log file;

diff -r 49afe0e92163 -r cc7990d6eb38 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 27 14:09:59 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 27 14:15:04 2012 +0200
@@ -481,9 +481,11 @@
             if (rc == 0) {
               val sources = make_stamp(name)
               val heap = heap_stamp(job.output_path)
+              (output_dir + log(name)).file.delete
               File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
             }
             else {
+              (output_dir + log_gz(name)).file.delete
               File.write(output_dir + log(name), out)
               echo(name + " FAILED")
               echo("(see also " + log(name).file.toString + ")")