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.

Sign up for GitHub

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

Jump to bottom

run docgen job only when pushing on master #37

Merged
merged 1 commit into from
Jun 16, 2020
Merged

run docgen job only when pushing on master #37

merged 1 commit into from
Jun 16, 2020

Conversation

rodonisi
Copy link
Collaborator

  • this should avoid having failing docgen builds when a PR and branch run try to push docs at the same time
  • also, this avoids overwriting the current docs with potentially uncompleted docs or docs from experimental operations

run docgen job only when pushing on master
159f353 
* this should avoid having failing docgen builds when a PR and branch run try to push docs at the same time
* also this avoids overwriting the current docs with potentially uncompleted docs or docs from experimental operations
@rodonisi rodonisi requested a review from maerhart June 16, 2020 10:10
maerhart
maerhart approved these changes Jun 16, 2020
View reviewed changes
Copy link
Owner

@maerhart maerhart left a comment

Choose a reason for hiding this comment

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

That's a really nice addition!
One question though: can't we get rid of the action on pull_request altogether?
As far as I could notice they always do the same in PRs, or am I missing something?

@rodonisi
Copy link
Collaborator Author

I'm not sure I understand it correctly, but it does run the test as if the PR was merged into master, doesn't it?
If that's correct I think it's useful to have in cases where the PR gets our of sync from master and could break something that is not yet on the PR branch, which did not happen yet in our case.

@maerhart
Copy link
Owner

That would make sense. So let's just leave it in there for now.

@maerhart maerhart merged commit 2357390 into master Jun 16, 2020
@maerhart maerhart deleted the feature-push-docs-master branch June 16, 2020 13:43
@rodonisi
Copy link
Collaborator Author

Thanks for the quick merge!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maerhart maerhart maerhart approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@rodonisi @maerhart