src/Pure/library.scala

--- a/src/Pure/library.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/library.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -82,10 +82,6 @@
     else ""
   }
 
-  def trim_line(str: String): String =
-    if (str.endsWith("\n")) str.substring(0, str.length - 1)
-    else str
-
   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)