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

ci/update: re-apply manual commits from open PR #2940

Merged
merged 2 commits into from
Jan 30, 2025
Merged

Conversation

MattSturgeon
Copy link
Member

@MattSturgeon MattSturgeon commented Jan 30, 2025

Using git cherry-pick, we can re-apply any manually committed changes in the already open PR. "Manually committed" is defined as any commit after the most recent commit authored by github-actions[bot].

We can also check if any files have differences before pushing.

This removes the inputs.nixpkgs revision checking added in #2885, because the new file-differences check is simpler and more useful.

A major benefit of re-applying the additional commits is that they are no longer lost when the CI force-pushes its updates.

This has been tested:

Also: the second commit fixes a bug in #2935 where the create-pr step was checking an undefined variable.

Instead of comparing the nixpkgs input revision, we can re-apply any
manually committed changes and then check if any files are different
before pushing.
@MattSturgeon MattSturgeon requested a review from a team January 30, 2025 21:39
@MattSturgeon
Copy link
Member Author

@mergify queue

Copy link
Contributor

mergify bot commented Jan 30, 2025

queue

✅ The pull request has been merged automatically

The pull request has been merged automatically at 93df574

Copy link
Contributor

mergify bot commented Jan 30, 2025

This pull request, with head sha 93df574b42928d631d31fe312cadb3899eb5b1bd, has been successfully merged with fast-forward by Mergify.

This pull request will be automatically closed by GitHub.

As soon as GitHub detects that the sha 93df574b42928d631d31fe312cadb3899eb5b1bd is part of the main branch, it will mark this pull request as merged.

It is possible for this pull request to remain open if this detection does not happen, this usually happens when a force-push is done on this branch ci/apply_pr_commits, this means GitHub will fail to detect the merge.

@mergify mergify bot merged commit 93df574 into main Jan 30, 2025
5 checks passed
@MattSturgeon MattSturgeon deleted the ci/apply_pr_commits branch January 30, 2025 22:11
@khaneliman
Copy link
Contributor

That's awesome, thanks!

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.

3 participants