From 428465d2f2af67f526cf6aabfe80a0aba8daf840 Mon Sep 17 00:00:00 2001
From: Q <q@moonq.org>
Date: Sat, 15 Jan 2022 21:17:27 +0200
Subject: [PATCH] unfold when selecting via menu

---
 index.html | 1 +
 1 file changed, 1 insertion(+)

diff --git a/index.html b/index.html
index f76fddb..0f11b3b 100644
--- 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="";
       };