You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
No, I've not yet found a way to do this for GitHub-based CI. But this need should be quite common, maybe someone found a solution and made an action / an app for this? I'm also happy to add custom support to coqbot for this (similar to what we did for GitLab CI in the main repo). The main question is how to host the generated HTML for the branch. In GitLab CI, it is automatically pushed to GitLab Pages under some specific path. If we could solve this, it would also benefit the Rocq Platform Docs project, which has the same issue.
Is there a way to see CI-built HTML documentation for an unmerged PR? Thanks!
The text was updated successfully, but these errors were encountered: