-
Notifications
You must be signed in to change notification settings - Fork 38
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
Changes from all commits
Commits
Show all changes
13 commits
Select commit
Hold shift + click to select a range
39fcf61
Add subpath redirect
huynhtrankhanh 4a53adc
Empty commit to force CI
huynhtrankhanh badbc17
Fix typo
huynhtrankhanh 3f411ba
Add refman redirect
huynhtrankhanh 43c08c4
Change to relative
huynhtrankhanh 7b13a9c
Change to relative
huynhtrankhanh 9a6bf19
Add refman redirect
huynhtrankhanh 5f00920
Oops I was dumb
huynhtrankhanh 3b0f1eb
Fix refman redirect
huynhtrankhanh c728f5f
Change to relative
huynhtrankhanh 78d6198
Change to relative
huynhtrankhanh 02061c0
Change to relative
huynhtrankhanh 5038407
Add stdlib distrib redirect
huynhtrankhanh File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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/"); | ||
} 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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
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
).There was a problem hiding this comment.
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)
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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.]
There was a problem hiding this comment.
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.