From 3bb538b03239c88adbddcb10a148c349ce5dce40 Mon Sep 17 00:00:00 2001
From: Gabor Kiss-Vamosi <kisvegabor@gmail.com>
Date: Mon, 11 Dec 2023 19:16:55 +0100
Subject: [PATCH] docs: add docs- prefix to link IDs in the banner

---
 docs/_static/js/custom.js | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/docs/_static/js/custom.js b/docs/_static/js/custom.js
index abbe54fe3..fa1327d60 100644
--- a/docs/_static/js/custom.js
+++ b/docs/_static/js/custom.js
@@ -41,7 +41,17 @@ document.addEventListener('DOMContentLoaded', (event) => {
     newP.innerHTML = data
     newDiv.insertBefore(newP, newDiv.firstChild);
 
-      }) .catch(error => {
+    const children = newDiv.querySelectorAll('*');
+
+    // Iterate over each child
+    children.forEach(child => {
+        // Check if the child has an id
+        if (child.id) {
+            // Prepend 'docs-' to the id
+            child.id = 'docs-' + child.id;
+        }
+    })
+  }) .catch(error => {
         console.error('Fetch error: ' + error.message);
-    });
+  });
 })