Skip to content
This repository has been archived by the owner. It is now read-only.

Fix #13: deduplicate pull request merge and push information #14

Merged
merged 1 commit into from Oct 6, 2018

Conversation

@TrueBrain
Copy link
Member

@TrueBrain TrueBrain commented Oct 6, 2018

When a PR is merged, there is no need to show the pushes it caused.
If anyone is interested, they can open up the PR for more
information. As the PR is more interesting than the pushes, the
latter is now ignored if it follows a PR merge.

When a PR is merged, there is no need to show the pushes it caused.
If anyone is interested, they can open up the PR for more
information. As the PR is more interesting than the pushes, the
latter is now ignored if it follows a PR merge.
@LordAro
Copy link
Member

@LordAro LordAro commented Oct 6, 2018

Does this work for PRs with multiple commits that get rebased/squashed onto the top, instead of a merge commit?

@TrueBrain
Copy link
Member Author

@TrueBrain TrueBrain commented Oct 6, 2018

I think so; I use the merge_commit_sha, which I hope is the sha of the last commit that is being merged. Not a lot of documentation there. We could try I guess. It would at least make it better, not worse ;)

LordAro
LordAro approved these changes Oct 6, 2018
@TrueBrain
Copy link
Member Author

@TrueBrain TrueBrain commented Oct 6, 2018

Tested both rebase and squash; both times the field merge_commit_sha was the after sha of the push that followed :)

@TrueBrain TrueBrain merged commit 58851d2 into OpenTTD:master Oct 6, 2018
1 check passed
@TrueBrain TrueBrain deleted the deduplicate branch Nov 10, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

2 participants