# HG changeset patch
# User wenzelm
# Date 1544468402 -3600
# Node ID eaf66384cfe852e199ca847c8b16647230b8ff7e
# Parent  22d4cb91ea6d08035f9e9e23cdba363e6ec78d48
clarified input_line: exclude terminator (its only use in Isabelle_Process.read_command is is unaffected, due to liberal Int.fromString);

diff -r 22d4cb91ea6d -r eaf66384cfe8 src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Sun Dec 09 20:19:31 2018 +0100
+++ b/src/Pure/System/system_channel.ML	Mon Dec 10 20:00:02 2018 +0100
@@ -21,7 +21,7 @@
 
 fun input_line (System_Channel (in_stream, _)) =
   let
-    fun result cs = String.implode (rev (#"\n" :: cs));
+    val result = trim_line o String.implode o rev;
     fun read cs =
       (case BinIO.input1 in_stream of
         NONE => if null cs then NONE else SOME (result cs)