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

diff --git a/doxygen/search.js b/doxygen/search.js
index 901593edf4fc3a9f2d49ae3cb721847d91855737..6031ca5d268b6a04c77a867d1e398cef5f443a60 100644 (file)
--- 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';
 }