src/Pure/library.scala

--- a/src/Pure/library.scala	Sun Jul 22 21:59:14 2012 +0200
+++ b/src/Pure/library.scala	Sun Jul 22 23:31:57 2012 +0200
@@ -62,6 +62,10 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
+  def trim_line(str: String): String =
+    if (str.endsWith("\n")) str.substring(0, str.length - 1)
+    else str
+
 
   /* iterate over chunks (cf. space_explode) */