# HG changeset patch
# User wenzelm
# Date 1476999555 -7200
# Node ID ff3c383b9163877641f3491dc3472fd905a13ba0
# Parent  47e03cb9927458fdd72f2405bfe2d45f7c570f46
extra trim_line for the sake of Windows;

diff -r 47e03cb99274 -r ff3c383b9163 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