From: Vladimír Vondruš <mosra@centrum.cz>
Date: Wed, 2 Jan 2019 21:01:51 +0000 (+0100)
Subject: doxygen: actually remove the ID attribute instead of emptying it.
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~cjwatson/git?a=commitdiff_plain;h=5cbdf20bd943f8f70e745f29f6b1d4ad5ef90291;p=blog.git

doxygen: actually remove the ID attribute instead of emptying it.
---

diff --git a/doxygen/search.js b/doxygen/search.js
index 901593ed..6031ca5d 100644
--- a/doxygen/search.js
+++ b/doxygen/search.js
@@ -580,7 +580,7 @@ function selectResult(event) {
     if(event.currentTarget.parentNode.id == 'search-current') return;
 
     let current = document.getElementById('search-current');
-    current.id = '';
+    current.removeAttribute('id');
     event.currentTarget.parentNode.id = 'search-current';
 }