1.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Nov 11 20:50:12 2013 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Nov 11 21:04:30 2013 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5      val writeln_buffer = Unsynchronized.ref Buffer.empty;
     1.6      fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
     1.7 -    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
     1.8 +    fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));
     1.9  
    1.10      val warnings = Unsynchronized.ref ([]: string list);
    1.11      fun warn msg = Unsynchronized.change warnings (cons msg);