src/Pure/System/build.scala
changeset 48626 ef374008cb7c
parent 48595 231e6fa96dbb
child 48639 675988e64bf9
equal deleted inserted replaced
48617:f4e9288fdbfc 48626:ef374008cb7c
   511             }
   511             }
   512             else {
   512             else {
   513               (output_dir + log_gz(name)).file.delete
   513               (output_dir + log_gz(name)).file.delete
   514               File.write(output_dir + log(name), out)
   514               File.write(output_dir + log(name), out)
   515               echo(name + " FAILED")
   515               echo(name + " FAILED")
   516               echo("(see also " + log(name).file.toString + ")")
   516               echo("(see also " + (output_dir + log(name)).file.toString + ")")
   517               val lines = split_lines(out)
   517               val lines = split_lines(out)
   518               val tail = lines.drop(lines.length - 20 max 0)
   518               val tail = lines.drop(lines.length - 20 max 0)
   519               echo("\n" + cat_lines(tail))
   519               echo("\n" + cat_lines(tail))
   520             }
   520             }
   521             loop(pending - name, running - name, results + (name -> (false, rc)))
   521             loop(pending - name, running - name, results + (name -> (false, rc)))