From 673a11b320b89785d67f721d22c4b61517bed392 Mon Sep 17 00:00:00 2001
From: Alex Maldonado <alex@scient.ing>
Date: Fri, 7 Aug 2026 20:37:22 -0400
Subject: [PATCH] fix: add missing docs-banner.html

---
 scripts/docs-banner.html | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 scripts/docs-banner.html

diff --git a/scripts/docs-banner.html b/scripts/docs-banner.html
new file mode 100644
index 0000000..5252c7c
--- /dev/null
+++ b/scripts/docs-banner.html
@@ -0,0 +1,14 @@
+<div style="padding:.4rem .75rem;font:0.85rem/1.4 sans-serif;border-bottom:1px solid var(--border-color,#ddd);background:var(--sidebar-background-color,#f7f7f7);color:var(--main-color,#000)">
+  Docs channel:
+  <a id="ch-release" href="#" style="margin:0 .35rem">release</a>|
+  <a id="ch-nightly" href="#" style="margin:0 .35rem">nightly</a>
+  <script>
+  (function () {
+    var m = location.pathname.match(/^(.*\/)(release|nightly)\//);
+    var base = m ? m[1] : location.pathname.replace(/[^\/]*$/, "");
+    document.getElementById("ch-release").href = base + "release/";
+    document.getElementById("ch-nightly").href = base + "nightly/";
+    if (m) { document.getElementById("ch-" + m[2]).style.fontWeight = "bold"; }
+  })();
+  </script>
+</div>