Add doc/index.md to redirect doc/ to the title page of the manual
#25
Conversation
This file contains hidden or 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
wilfwilson
changed the title
doc/index.md to redirect doc/ to the title page of the manualdoc/index.md to redirect doc/ to the title page of the manual
|
Actually, something else has to be changed (in this repo or in |
|
Perhaps I just need to add
|
wilfwilson
force-pushed
the
ww/doc/index.md
branch
from
d58215b to
afddbbb
Compare
wilfwilson
changed the title
doc/index.md to redirect doc/ to the title page of the manualdoc/index.html to redirect doc/ to the title page of the manual
wilfwilson
added a commit
to digraphs/Digraphs
that referenced
this pull request
Sep 20, 2025
…e manual This means that if a user requests https://digraphs.github.io/Digraphs/doc/ (which I think is a natural-enough thing to want to do), then instead of getting a 404 error, they are instead automatically redirected to the title page of the manual, which is presumably what they wanted, anyway. Unless and until gap-system/GitHubPagesForGAP#25 is merged, or gap-actions/update-gh-pages#10 is addressed in a way that lets us keeps this file purely in our gh-pages branch, then I think the best way to manage this file is to keep it in the repository here. Whenever the ReleaseTools script/release action is run, the doc/ directory of the gh-pages branch is deleted, and so if we only kept this file in the gh-pages branch, it would get deleted each time we make a new release. However, the doc/ directory of the gh-pages branch is re-populated with (amongst other things) the html files of the doc/ directory of this repository. In particular, by having this file in the doc/ directory of this repo, this means that the file is retained in the gh-pages branch, even across different releases of the package and runs of the ReleaseTools script/release action.
wilfwilson
added a commit
to wilfwilson/Digraphs
that referenced
this pull request
Sep 20, 2025
…e manual This means that if a user requests https://digraphs.github.io/Digraphs/doc/ (which I think is a natural-enough thing to want to do), then instead of getting a 404 error, they are instead automatically redirected to the title page of the manual, which is presumably what they wanted, anyway. Unless and until gap-system/GitHubPagesForGAP#25 is merged, or gap-actions/update-gh-pages#10 is addressed in a way that lets us keeps this file purely in our gh-pages branch, then I think the best way to manage this file is to keep it in the repository here. Whenever the ReleaseTools script/release action is run, the doc/ directory of the gh-pages branch is deleted, and so if we only kept this file in the gh-pages branch, it would get deleted each time we make a new release. However, the doc/ directory of the gh-pages branch is re-populated with (amongst other things) the html files of the doc/ directory of this repository. In particular, by having this file in the doc/ directory of this repo, this means that the file is retained in the gh-pages branch, even across different releases of the package and runs of the ReleaseTools script/release action.
|
I think the redirection makes a lot of sense. But this hardcodes links to Perhaps this could be a dynamic page that gets the |
wilfwilson
force-pushed
the
ww/doc/index.md
branch
from
afddbbb to
aa164e5
Compare
wilfwilson
changed the title
doc/index.html to redirect doc/ to the title page of the manualdoc/index.md to redirect doc/ to the title page of the manual
|
I've updated this as suggested by @stertooy, the file is now You can see this in action at https://wilfwilson.github.io/Digraphs/doc/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Perhaps there are nicer ways of doing this, I'm not sure. But at least this doesn't use javascript. I'm using this already for Digraphs: https://digraphs.github.io/Digraphs/doc/
Resolves #24.