JavaScript: toJSString doesn't support code points greater than 2^16
Due to the use of JavaScript's String.fromCharCode
in rts/js/string.js:h$fromHsString
, the conversion of large unicode code points is getting silently truncated to the lower 16 bits of the value (see https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/fromCharCode). The correct function here is String.fromCodePoint
(https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/fromCodePoint), which performs the conversion to UTF-16.