Set default version to main with mike 2.1.3

Docs Deploy · Docs Deploy · commit e46b2e40d999 · 2025-05-14T20:46:09.000Z
diff --git a/index.html b/index.html
@@ -8,11 +8,11 @@
   </noscript>
   <script>
     window.location.replace(
-      "main/docs/" + window.location.search + window.location.hash
+      "main/" + window.location.search + window.location.hash
     );
   </script>
 </head>
 <body>
-  Redirecting to <a href="main/docs/">main/</a>...
+  Redirecting to <a href="main/">main/</a>...
 </body>
 </html>
