author | wenzelm |
Thu, 20 Oct 2016 23:39:15 +0200 | |
changeset 64326 | ff3c383b9163 |
parent 64325 | 47e03cb99274 |
child 64327 | 3e651d9ce601 |
--- 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