diff -r 13282f91e6ff -r 27d298c6f961 svghmi/svghmi.js
--- a/svghmi/svghmi.js	Fri Jun 24 09:24:19 2022 +0200
+++ b/svghmi/svghmi.js	Fri Jun 24 10:46:26 2022 +0200
@@ -229,8 +229,8 @@
     return(Array.prototype.map.call(elt.children, x=>x.textContent).join("\\\\n")); 
 }
 
-function multiline_to_svg_text(elt, str) {
-    str.split('\\\\n').map((line,i) => {elt.children[i].textContent = line;});
+function multiline_to_svg_text(elt, str, blank) {
+    str.split('\\\\n').map((line,i) => {elt.children[i].textContent = blank?"":line;});
 }
 
 function switch_langnum(langnum) {