From 5cbdf20bd943f8f70e745f29f6b1d4ad5ef90291 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Vladim=C3=ADr=20Vondru=C5=A1?= Date: Wed, 2 Jan 2019 22:01:51 +0100 Subject: [PATCH] doxygen: actually remove the ID attribute instead of emptying it. --- doxygen/search.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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'; } -- 2.30.2