author | wenzelm |
Sat, 12 Nov 2022 19:09:41 +0100 (2022-11-12) | |
changeset 76512 | c3b4e5e4c4e5 |
parent 76511 | ec8c04dac257 |
child 76513 | 5a9a82522266 |
--- a/src/Pure/Tools/prismjs.scala Sat Nov 12 19:04:28 2022 +0100 +++ b/src/Pure/Tools/prismjs.scala Sat Nov 12 19:09:41 2022 +0100 @@ -41,7 +41,7 @@ """ function prismjs_content(t) { if (t instanceof prismjs.Token) { return prismjs_content(t.content) } - else if (Array.isArray(t)) { return t.map(prismjs_content).join() } + else if (Array.isArray(t)) { return t.map(prismjs_content).join("") } else { return t } }