828d707465
When redirecting from old-topic.html#some-id to new-topic.html, the ID is ignored. Not sure if it is possible to keep the ID in the meta redirect, but at least in the JavaScript version we should keep it and redirect from old-topic.html#some-id to new-topic.html#some-id. Signed-off-by: Ruth Fuchss <ruth.fuchss@nordicsemi.no>
81 lines
2.4 KiB
Python
81 lines
2.4 KiB
Python
# Copyright 2018-2019 Espressif Systems (Shanghai) PTE LTD
|
|
#
|
|
# Licensed under the Apache License, Version 2.0 (the "License");
|
|
# you may not use this file except in compliance with the License.
|
|
# You may obtain a copy of the License at
|
|
#
|
|
# http://www.apache.org/licenses/LICENSE-2.0
|
|
#
|
|
# Unless required by applicable law or agreed to in writing, software
|
|
# distributed under the License is distributed on an "AS IS" BASIS,
|
|
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
# See the License for the specific language governing permissions and
|
|
# limitations under the License.
|
|
#
|
|
|
|
|
|
# Mechanism to generate static HTML redirect pages in the output
|
|
#
|
|
# Uses redirect_template.html and the list of pages given in
|
|
# conf.html_redirect_pages
|
|
#
|
|
# Adapted from ideas in https://tech.signavio.com/2017/managing-sphinx-redirects
|
|
import os.path
|
|
|
|
from sphinx.builders.html import StandaloneHTMLBuilder
|
|
|
|
REDIRECT_TEMPLATE = r"""
|
|
<html>
|
|
<head>
|
|
<meta http-equiv="refresh" content="0; url=$NEWURL" />
|
|
<script>
|
|
var id=window.location.href.split("#")[1];
|
|
|
|
if (id && (/^[a-zA-Z\:\/0-9\_\-\.]+$/.test(id))) {
|
|
window.location.href = "$NEWURL"+"#"+id;
|
|
}
|
|
else {
|
|
window.location.href = "$NEWURL";
|
|
};
|
|
</script>
|
|
</head>
|
|
<body>
|
|
<p>Page has moved <a href="$NEWURL">here</a>.</p>
|
|
</body>
|
|
</html>
|
|
"""
|
|
|
|
|
|
def setup(app):
|
|
app.add_config_value('html_redirect_pages', [], 'html')
|
|
app.connect('build-finished', create_redirect_pages)
|
|
|
|
# Since we're just setting up a build-finished hook, which runs
|
|
# after both reading and writing, this extension is safe for both.
|
|
return {
|
|
'parallel_read_safe': True,
|
|
'parallel_write_safe': True,
|
|
}
|
|
|
|
|
|
def create_redirect_pages(app, docname):
|
|
if not isinstance(app.builder, StandaloneHTMLBuilder):
|
|
return # only relevant for standalone HTML output
|
|
|
|
for (old_url, new_url) in app.config.html_redirect_pages:
|
|
if old_url.startswith('/'):
|
|
old_url = old_url[1:]
|
|
|
|
new_url = app.builder.get_relative_uri(old_url, new_url)
|
|
out_file = app.builder.get_outfilename(old_url)
|
|
|
|
out_dir = os.path.dirname(out_file)
|
|
if not os.path.exists(out_dir):
|
|
os.makedirs(out_dir)
|
|
|
|
content = REDIRECT_TEMPLATE.replace("$NEWURL", new_url)
|
|
|
|
if not os.path.exists(out_file):
|
|
with open(out_file, "w") as rp:
|
|
rp.write(content)
|