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