--- a/src/Pure/General/output.scala Fri May 02 19:51:40 2014 +0200
+++ b/src/Pure/General/output.scala Fri May 02 20:01:45 2014 +0200
@@ -12,8 +12,8 @@
def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
- def writeln(msg: String) { System.err.println(msg) }
- def warning(msg: String) { System.err.println(warning_text(msg)) }
- def error_message(msg: String) { System.err.println(error_text(msg)) }
+ def writeln(msg: String) { Console.err.println(msg) }
+ def warning(msg: String) { Console.err.println(warning_text(msg)) }
+ def error_message(msg: String) { Console.err.println(error_text(msg)) }
}