fix: add missing docs-banner.html

2026-08-07 20:37:22 -04:00
parent 717c4b412a
commit 673a11b320
1 changed files with 14 additions and 0 deletions
@@ -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>