# HG changeset patch # User wenzelm # Date 1343749233 -7200 # Node ID ef374008cb7cf66334945328e36855a5bb2dc30f # Parent f4e9288fdbfceb5d1a0083f502ad586542752709 print full path; diff -r f4e9288fdbfc -r ef374008cb7c src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Jul 31 16:26:12 2012 +0200 +++ b/src/Pure/System/build.scala Tue Jul 31 17:40:33 2012 +0200 @@ -513,7 +513,7 @@ (output_dir + log_gz(name)).file.delete File.write(output_dir + log(name), out) echo(name + " FAILED") - echo("(see also " + log(name).file.toString + ")") + echo("(see also " + (output_dir + log(name)).file.toString + ")") val lines = split_lines(out) val tail = lines.drop(lines.length - 20 max 0) echo("\n" + cat_lines(tail))