unfold when selecting via menu

2022-01-15 21:17:27 +02:00
parent e5531496ee
commit 428465d2f2
1 changed files with 1 additions and 0 deletions
--- a/index.html
+++ b/index.html
@@ -125,6 +125,7 @@ function make_menu() {
        document.getElementById(this.value).scrollIntoView();
        var head=this.value.replace(/^anchor/,"head");
        document.getElementById(head).classList.add("blink");
+        fold_set(head.replace("head_",""),false);
        setTimeout(function(){ document.getElementById(head).classList.remove("blink"); }, 3000);
        document.getElementById("menu").value="";
      };