# HG changeset patch
# User wenzelm
# Date 1668276581 -3600
# Node ID c3b4e5e4c4e52171463045db191b33399966b424
# Parent  ec8c04dac257b64eb3fa83f8efcae8dbab3d47f0
proper join without delimiter;

diff -r ec8c04dac257 -r c3b4e5e4c4e5 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 }
 }