-
Notifications
You must be signed in to change notification settings - Fork 108
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
Automate GitHub Pages generation #477
Comments
possible duplicate of #291 |
You could just check those pages into |
I'll close this since it's a duplicate. About checking in to |
Oh I just meant if there were a fixed set of extra static landing pages you could check them in somewhere. The main suggestion was to use GitHub actions to generate the gh-pages. GitHub actions could also generate these static pages as well. |
I'm not sure if I follow. |
If we move to a world where gh-pages is an automatically built branch, then one setup would be to just deploy clean to it every time master is updated by rebuilding the html pages in GitHub actions. @dan-zheng was worried that this would make it difficult to also have manually created html pages there. One solution would be to move those manual pages somewhere else, another would be to only update the non manual part of the branch, a final solution would be to have no manual pages and just autogen placeholders. This is not an interesting problem. |
Task
We can use GitHub Actions to automate GitHub Pages updates: running
make docs
and pushing the output togh-pages
branch. So far, we've been updatinggh-pages
branch manually.Automation suggested here: #472 (comment)
Considerations
gh-pages
branch currently has some hardcoded stop-gap HTML redirection pages, added in Add HTML redirection pages. #392. We should consider what to do with those - maybe we're okay with dropping those pages by now.The text was updated successfully, but these errors were encountered: