author | wenzelm |
Thu, 04 May 2017 15:10:51 +0200 | |
changeset 65718 | 79be5b464a16 |
parent 65717 | 556c34fd0554 |
child 65720 | c5b19f997214 |
child 65721 | 01fc771021e6 |
--- a/src/Pure/library.scala Thu May 04 14:58:19 2017 +0200 +++ b/src/Pure/library.scala Thu May 04 15:10:51 2017 +0200 @@ -145,7 +145,7 @@ def trim_substring(s: String): String = new String(s.toCharArray) def proper_string(s: String): Option[String] = - if (s == "") None else Some(s) + if (s == null || s == "") None else Some(s) /* quote */