extra trim_line for the sake of Windows;
authorwenzelm
Thu, 20 Oct 2016 23:39:15 +0200
changeset 64326 ff3c383b9163
parent 64325 47e03cb99274
child 64327 3e651d9ce601
extra trim_line for the sake of Windows;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Oct 20 23:05:13 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 20 23:39:15 2016 +0200
@@ -176,7 +176,7 @@
         val line_buffer = new ByteArrayOutputStream(100)
         def line_flush()
         {
-          val line = line_buffer.toString(UTF8.charset_name)
+          val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
           progress(line)
           result += line
           line_buffer.reset