# 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