mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix error-index redirect to work with back button.

Browse Source
This commit is contained in:
Eric Huss 2023-01-05 11:07:11 -08:00
parent e94fab69d0
commit f2ad85a930
2 changed files with 10 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/tools/error_index_generator/main.rs
View File

@ -98,8 +98,7 @@ fn add_rust_attribute_on_codeblock(explanation: &str) -> String {
fn render_html(output_path: &Path) -> Result<(), Box<dyn Error>> {
let mut introduction = format!(
"<script src='redirect.js'></script>
# 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.
</head>
<body>
<div>If you are not automatically redirected to the error code index, please <a id="index-link" href="./error_codes/error-index.html">here</a>.
<script>document.getElementById("index-link").click()</script>
</body>
</html>"#,
)?;

10
src/tools/error_index_generator/redirect.js
View File

@ -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');
})()