proper join without delimiter;
authorwenzelm
Sat, 12 Nov 2022 19:09:41 +0100 (2022-11-12)
changeset 76512 c3b4e5e4c4e5
parent 76511 ec8c04dac257
child 76513 5a9a82522266
proper join without delimiter;
src/Pure/Tools/prismjs.scala
--- 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 }
 }