Skip to content

Conversation

@adomasbaliuka
Copy link
Contributor

No description provided.

@adomasbaliuka adomasbaliuka mentioned this pull request Jan 19, 2026
@adomasbaliuka adomasbaliuka marked this pull request as draft January 19, 2026 09:37
@adomasbaliuka
Copy link
Contributor Author

adomasbaliuka commented Jan 19, 2026

It worked on my fork: https://adomasbaliuka.github.io/interval/docs/

I'm assuming it would work for the main repository if merged (and I hope it shouldn't work from a PR since otherwise anyone could just deploy a website to someone else's domain... I hope the GITHUB_TOKEN permissions take care of this).

Note: in the current configuration, every CI run (on any branch) always overwrites the deployed docs. I think that's bad (and only just realized this) so let's not merge until I find a solution.

@girving
Copy link
Owner

girving commented Jan 19, 2026

Looks good to me, but I don’t know to test it further without just merging. I can’t merge when it’s marked as a draft though. Want to take off the draft status, and we can try it out?

Oops, sorry, reading comprehension failure: I only just parsed your overwrite comment. :)

@adomasbaliuka adomasbaliuka marked this pull request as ready for review January 20, 2026 10:53
@adomasbaliuka
Copy link
Contributor Author

Added an if to only run the "API-docs" step on the main branch. I tested this on my other repository and it works.

There doesn't seem to be a straightforward way to "build but not deploy" the docs (e.g., to inspect what a PR does to them before merging, see leanprover-community/docgen-action#9), but I guess that's fine.

@girving girving merged commit 7121e66 into girving:main Jan 20, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants