Skip to content
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

Allow building full docs in PR, opt-in #3800

Merged
merged 6 commits into from
Jan 9, 2023
Merged

Conversation

MatthewFlamm
Copy link
Contributor

@MatthewFlamm MatthewFlamm commented Jan 9, 2023

Overview

Allow adding a label to build full docs.

Details

This is opt-in from the perspective of the labelling. PR authors without label write permissions do not have the optionality.

@github-actions github-actions bot added the maintenance Low-impact maintenance activity label Jan 9, 2023
@MatthewFlamm MatthewFlamm added the full-doc Run full documentation build on CI label Jan 9, 2023
@MatthewFlamm
Copy link
Contributor Author

MatthewFlamm commented Jan 9, 2023

As of now, this PR will only work if the label pre-exists when a commit is pushed. I will push a dummy commit to test. To finish this, we should also run the doc build if when a PR is labeled with full-doc.

@codecov
Copy link

codecov bot commented Jan 9, 2023

Codecov Report

Merging #3800 (55c4a29) into main (bda7d71) will not change coverage.
The diff coverage is n/a.

❗ Current head 55c4a29 differs from pull request most recent head a6c2b69. Consider uploading reports for the commit a6c2b69 to get more accurate results

@@           Coverage Diff           @@
##             main    #3800   +/-   ##
=======================================
  Coverage   94.15%   94.15%           
=======================================
  Files          86       86           
  Lines       18891    18891           
=======================================
  Hits        17787    17787           
  Misses       1104     1104           

@MatthewFlamm MatthewFlamm added full-doc Run full documentation build on CI partially-solved For issues that have been addressed but not solved and removed full-doc Run full documentation build on CI partially-solved For issues that have been addressed but not solved labels Jan 9, 2023
@@ -25,6 +26,8 @@ env:

jobs:
doc:
# Don't run if we labeled with a label other than `full-doc`
if: ${{ !(github.event.action == 'labeled' && github.event.label.name != 'full-doc') }}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't work if any other labeled is added. It will still start the action but not run doc. This leads to the check not showing up in the PR. Unless we want to run this action everytime a label is added (I wouldn't recommend as we could be adding labels right before merging), I think we will have to push commits to get this label to work. It isn't a big hurdle IMO.

@MatthewFlamm MatthewFlamm marked this pull request as ready for review January 9, 2023 14:57
@MatthewFlamm
Copy link
Contributor Author

Doc build fails as expected here, as I labeled it before pushing the last commit.

@banesullivan banesullivan merged commit dd42c05 into main Jan 9, 2023
@banesullivan banesullivan deleted the maint/allow-full-doc-in-PR branch January 9, 2023 16:01
@banesullivan banesullivan mentioned this pull request Feb 1, 2023
5 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
full-doc Run full documentation build on CI maintenance Low-impact maintenance activity
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants