--- a/src/Pure/ML/ml_compiler_polyml.ML Mon Aug 10 11:20:16 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Aug 10 11:23:49 2015 +0200
@@ -153,8 +153,8 @@
val error_buffer = Unsynchronized.ref Buffer.empty;
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
- fun flush_error () = #writeln flags (Buffer.content (! error_buffer));
- fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
+ fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
+ fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
fun message {message = msg, hard, location = loc, context = _} =
let