Skip to content

Conversation

ararslan
Copy link
Member

There were no functional changes between #5904 and now; all that should be needed is the version change. Once merged, I'll revert this with [skip build].

@giordano
Copy link
Member

I'll revert this with [skip build].

And [skip ci] upon merging (but not in the PR, otherwise CI will never run and the PR can't be merged)

@giordano giordano merged commit c5abf23 into master Sep 27, 2024
21 checks passed
@giordano giordano deleted the aa/rebuild-old-mpfr branch September 27, 2024 19:09
@ararslan
Copy link
Member Author

Checking my understanding: I put [skip build] in the commit message for the commit I push to a branch, and I include [skip ci] in the commit message that GitHub allows you to edit when merging the PR?

@giordano
Copy link
Member

Correct

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