Docs: Take into account the anchor when redirecting.

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

Showing with 7 additions and 3 deletions

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

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

 list_redirects = [('reference/language_basics', 'userguide/language_basics')]