Put back the fallback for the case javascript is disabled and also handle the case with no anchor.

56f96fe5 · gabrieldemarmiesse · 0a0a9038 · 56f96fe5
Commit 56f96fe5 authored Jul 07, 2018 by gabrieldemarmiesse
Show whitespace changes
Inline Side-by-side

Showing with 9 additions and 3 deletions

docs/conf.py docs/conf.py +9 -3

No files found.
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -463,12 +463,18 @@ html_template = """
 <html>
    <head>
        <script>
+            // Redirect to the new-style URL
+            var new_location = '{0}'
+            
            // Some browsers include the hash character in the anchor, strip it out
            const anchor = window.location.hash.replace(/^#(.*)/, '$1');
+            if (anchor){{
+                new_location += '#' + anchor;
+            }}
            
-            // Redirect to the new-style URL
-            window.location = '{}#' + anchor;
+            window.location = new_location
        </script>
+        <meta http-equiv="refresh" content="1; url={0}:" />
    </head>
 </html>
 """