changeset 65715 | e57e5935c6b4 |
parent 65712 | ddd6dfc28e80 |
child 65718 | 79be5b464a16 |
--- a/src/Pure/library.scala Thu May 04 12:27:18 2017 +0200 +++ b/src/Pure/library.scala Thu May 04 12:30:19 2017 +0200 @@ -147,9 +147,6 @@ def proper_string(s: String): Option[String] = if (s == "") None else Some(s) - def proper_string_default(s: String, default: => String): String = - if (s == "") default else s - /* quote */