# HG changeset patch
# User wenzelm
# Date 1439198629 -7200
# Node ID 9f45c2f1cbfdfb0b75b4d8760321d19afd0614e6
# Parent  9b26f3118e40f17d3161b4c59f080e7ecb6e5b84
tuned messages;

diff -r 9b26f3118e40 -r 9f45c2f1cbfd src/Pure/ML/ml_compiler_polyml.ML
--- 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