changeset 65718 | 79be5b464a16 |
parent 65715 | e57e5935c6b4 |
child 65761 | ce909161d030 |
--- 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 */