author | wenzelm |
Fri, 18 Dec 2009 12:10:52 +0100 | |
changeset 34118 | ee9f87e11400 |
parent 34117 | 1eb8d8e3e40a |
child 34119 | ae92efb48784 |
--- a/src/Pure/General/yxml.scala Fri Dec 18 11:44:25 2009 +0100 +++ b/src/Pure/General/yxml.scala Fri Dec 18 12:10:52 2009 +0100 @@ -60,7 +60,8 @@ def flush() { if (code != -1) { - if (rest == 0) buf.appendCodePoint(code) + if (rest == 0 && Character.isValidCodePoint(code)) + buf.appendCodePoint(code) else buf.append('\uFFFD') code = -1 rest = 0