Added navbar and removed insert_navbar.sh

TuringLang · Dec 29, 2024 · cc0a71d · cc0a71d
1 parent a44c234
commit cc0a71d
Show file tree

Hide file tree

Showing 531 changed files with 1,062 additions and 1,062 deletions.
diff --git a/dev/chains/index.html b/dev/chains/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/diagnostics/index.html b/dev/diagnostics/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/gadfly/index.html b/dev/gadfly/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/getting-started/index.html b/dev/getting-started/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/index.html b/dev/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/makie/index.html b/dev/makie/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/modelstats/index.html b/dev/modelstats/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/stats/index.html b/dev/stats/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/statsplots/index.html b/dev/statsplots/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/dev/summarize/index.html b/dev/summarize/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/chains/index.html b/previews/PR280/chains/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/diagnostics/index.html b/previews/PR280/diagnostics/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/gadfly/index.html b/previews/PR280/gadfly/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/getting-started/index.html b/previews/PR280/getting-started/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/index.html b/previews/PR280/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/modelstats/index.html b/previews/PR280/modelstats/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/search/index.html b/previews/PR280/search/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/stats/index.html b/previews/PR280/stats/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/statsplots/index.html b/previews/PR280/statsplots/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR280/summarize/index.html b/previews/PR280/summarize/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR288/chains/index.html b/previews/PR288/chains/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");

diff --git a/previews/PR288/diagnostics/index.html b/previews/PR288/diagnostics/index.html
@@ -375,7 +375,7 @@
             </g>
         </svg>
     </a>
-    <span class="ext-menu-toggle"><body>#9776;</span>
+    <span class="ext-menu-toggle">&#9776;</span>
 </nav>
 <script>
     document.addEventListener("DOMContentLoaded", function () {
@@ -413,7 +413,7 @@
         // Close menus if clicked outside
         document.addEventListener("click", (event) => {
             if (
-                !navLinks.contains(event.target) <body><body>
+                !navLinks.contains(event.target) &&
                 !menuToggle.contains(event.target)
             ) {
                 navLinks.classList.remove("show");