From f2ad85a930539986517747729df6082553d195f8 Mon Sep 17 00:00:00 2001 From: Eric Huss Date: Thu, 5 Jan 2023 11:07:11 -0800 Subject: [PATCH] Fix error-index redirect to work with back button. --- src/tools/error_index_generator/main.rs | 11 +++++++---- src/tools/error_index_generator/redirect.js | 10 +++------- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/tools/error_index_generator/main.rs b/src/tools/error_index_generator/main.rs index 1bde8e00782..2ccb6b81233 100644 --- a/src/tools/error_index_generator/main.rs +++ b/src/tools/error_index_generator/main.rs @@ -98,8 +98,7 @@ fn add_rust_attribute_on_codeblock(explanation: &str) -> String { fn render_html(output_path: &Path) -> Result<(), Box> { let mut introduction = format!( - " -# Rust error codes index + "# Rust error codes index This page lists all the error codes emitted by the Rust compiler. @@ -149,7 +148,12 @@ This page lists all the error codes emitted by the Rust compiler. book.book.sections.push(BookItem::Chapter(chapter)); book.build()?; - // We can't put this content into another file, otherwise `mbdbook` will also put it into the + // The error-index used to be generated manually (without mdbook), and the + // index was located at the top level. Now that it is generated with + // mdbook, error-index.html has moved to error_codes/error-index.html. + // This adds a redirect so that old links go to the new location. + // + // We can't put this content into another file, otherwise `mdbook` will also put it into the // output directory, making a duplicate. fs::write( output_path.join("error-index.html"), @@ -163,7 +167,6 @@ This page lists all the error codes emitted by the Rust compiler.
If you are not automatically redirected to the error code index, please here. - "#, )?; diff --git a/src/tools/error_index_generator/redirect.js b/src/tools/error_index_generator/redirect.js index 8c907f5795d..c80cbf297af 100644 --- a/src/tools/error_index_generator/redirect.js +++ b/src/tools/error_index_generator/redirect.js @@ -3,14 +3,10 @@ let code = window.location.hash.replace(/^#/, ''); // We have to make sure this pattern matches to avoid inadvertently creating an // open redirect. - if (!/^E[0-9]+$/.test(code)) { + if (/^E[0-9]+$/.test(code)) { + window.location.replace('./error_codes/' + code + '.html'); return; } - if (window.location.pathname.indexOf("/error_codes/") !== -1) { - // We're not at the top level, so we don't prepend with "./error_codes/". - window.location = './' + code + '.html'; - } else { - window.location = './error_codes/' + code + '.html'; - } } + window.location.replace('./error_codes/error-index.html'); })()