changeset 52444 | 2cfe6656d6d6 |
parent 51983 | 32692ce4c61a |
child 54548 | 41e4ba92a979 |
--- a/src/Pure/library.scala Tue Jun 25 11:41:16 2013 +0200 +++ b/src/Pure/library.scala Tue Jun 25 12:17:19 2013 +0200 @@ -107,6 +107,11 @@ def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None + def trim_line(s: String): String = + if (s.endsWith("\r\n")) s.substring(0, s.length - 2) + else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) + else s + /* quote */