diff --git a/docs/_ext/externalredirect.py b/docs/_ext/externalredirect.py index 9319d10ba..86099ec7f 100644 --- a/docs/_ext/externalredirect.py +++ b/docs/_ext/externalredirect.py @@ -16,6 +16,13 @@ TEMPLATE = """ """ +SRC_TEMPLATE = """========== +File moved +========== + +This document has moved to %s. +This placeholder file will be removed in a later release. +""" def generate_external_redirects(app, exception): logger = logging.getLogger(__name__) @@ -48,7 +55,7 @@ def generate_external_redirects(app, exception): with open(path) as redirects: for line in redirects.readlines(): from_path, to_url = line.rstrip().split(' ') - + orig_from_path = from_path logger.info("Redirecting '%s' to '%s'" % (from_path, to_url)) if dirhtml: @@ -67,6 +74,10 @@ def generate_external_redirects(app, exception): with open(redirected_filename, 'w') as f: f.write(TEMPLATE % to_url) + input_rst_filename = os.path.join(app.srcdir, orig_from_path) + with open(input_rst_filename, 'w') as f: + f.write(SRC_TEMPLATE % to_url) + def setup(app): app.add_config_value('external_redirects_file', 'external_redirects', 'env')