Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add subpath redirects #232

Merged
merged 13 commits into from
Oct 12, 2023
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,4 +46,4 @@ jobs:
steps:
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v2
uses: actions/deploy-pages@v2
18 changes: 18 additions & 0 deletions pages/404.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
<#include "incl/macros.html">
<script>
const path = window.location.pathname;
const stdlibRegex = /^\/(stdlib|library)\//;
const refmanRegex = /^\/distrib\/(.*)\/refman\//;
const stdlibDistribRegex = /^\/distrib\/(.*)\/stdlib\//;
if (stdlibRegex.test(path)) {
window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
} else if (refmanRegex.test(path)) {
const version = path.match(refmanRegex)[1];
window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The case of distrib/current/refman will need to be handled specially (using the #CURRENTVERSIONTAG). BTW, this case also exists for the stdlib doc (as in /distrib/current/stdlib or /distrib/<version>/stdlib).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The distrib/current/refman is already handled by meta refresh redirect (https://htk-coq-website-fix.github.io/distrib/current/refman)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The same goes for /distrib/current/stdlib

Copy link
Member

@Zimmi48 Zimmi48 Oct 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This actually does not handle sub-paths. Here is an example of broken URL: https://htk-coq-website-fix.github.io/doc/current/refman/addendum/type-classes.html (already broken before this PR of course). [And here is one for the stdlib: https://htk-coq-website-fix.github.io/distrib/current/stdlib/Coq.Logic.Classical_Prop.html.]

Copy link
Member

@Zimmi48 Zimmi48 Oct 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've pushed a fix for this on master after merging your PR. Unfortunately, I couldn't push it on the PR first to test it with your fork, probably because your master branch is protected. Hopefully, it'll work on the first attempt. EDIT: It did.

} else if (stdlibDistribRegex.test(path)) {
const version = path.match(stdlibDistribRegex)[1];
window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/");
} else {
document.write("<h1>Not found</h1>");
}
</script>
4 changes: 2 additions & 2 deletions pages/distrib/current/refman/changes.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<#include "incl/macros.html">
<head>
<meta http-equiv="Refresh" content="0; URL=https://coq.github.io/doc/<#CURRENTVERSIONTAG>/refman/changes.html" />
</head>
<meta http-equiv="Refresh" content="0; URL=/doc/<#CURRENTVERSIONTAG>/refman/changes.html" />
</head>
2 changes: 1 addition & 1 deletion pages/distrib/current/refman/index.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<#include "incl/macros.html">
<head>
<meta http-equiv="Refresh" content="0; URL=https://coq.github.io/doc/<#CURRENTVERSIONTAG>/refman/" />
<meta http-equiv="Refresh" content="0; URL=/doc/<#CURRENTVERSIONTAG>/refman/" />
</head>
2 changes: 1 addition & 1 deletion pages/distrib/current/stdlib/index.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<#include "incl/macros.html">
<head>
<meta http-equiv="Refresh" content="0; URL=https://coq.github.io/doc/<#CURRENTVERSIONTAG>/stdlib/" />
<meta http-equiv="Refresh" content="0; URL=/doc/<#CURRENTVERSIONTAG>/stdlib/" />
</head>
2 changes: 1 addition & 1 deletion pages/library/index.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<#include "incl/macros.html">
<head>
<meta http-equiv="Refresh" content="0; URL=https://coq.github.io/doc/<#CURRENTVERSIONTAG>/stdlib/" />
<meta http-equiv="Refresh" content="0; URL=/doc/<#CURRENTVERSIONTAG>/stdlib/" />
</head>
2 changes: 1 addition & 1 deletion pages/stdlib/index.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<#include "incl/macros.html">
<head>
<meta http-equiv="Refresh" content="0; URL=https://coq.github.io/doc/<#CURRENTVERSIONTAG>/stdlib/" />
<meta http-equiv="Refresh" content="0; URL=/doc/<#CURRENTVERSIONTAG>/stdlib/" />
</head>
Loading