[Merged by Bors] - chore(CI): fix merge conflict resolution for nightly-testing#40257
Closed
Garmelon wants to merge 1 commit into
Closed
[Merged by Bors] - chore(CI): fix merge conflict resolution for nightly-testing#40257Garmelon wants to merge 1 commit into
Garmelon wants to merge 1 commit into
Conversation
PR summary 4eff6a086eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
Contributor
|
bors merge |
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Jun 15, 2026
Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see #40189 (see [#PR reviews > #39443 `nonempty_preimage_iff` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
Contributor
|
Pull request successfully merged into master. Build succeeded:
|
felixpernegger
pushed a commit
to felixpernegger/mathlib4
that referenced
this pull request
Jun 16, 2026
…ver-community#40257) Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
gasparattila
pushed a commit
to gasparattila/mathlib4
that referenced
this pull request
Jun 16, 2026
…ver-community#40257) Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
xroblot
pushed a commit
to xroblot/mathlib4
that referenced
this pull request
Jun 18, 2026
…ver-community#40257) Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
ReemMelamed
pushed a commit
to ReemMelamed/mathlib4
that referenced
this pull request
Jun 20, 2026
…ver-community#40257) Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
bryangingechen
pushed a commit
to jcommelin/mathlib4
that referenced
this pull request
Jun 22, 2026
…ver-community#40257) Resolving merge conflicts in favor of `nightly-testing` when merging `master` may be convenient for nightly maintainers, but it can lead to changes made on `master` accidentally being dropped again later in the bump PR. For an example case, see leanprover-community#40189 (see [#PR reviews > leanprover-community#39443 &leanprover-community#96;nonempty_preimage_iff&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339443.20.60nonempty_preimage_iff.60/near/599885755) for an explanation of what happened). Resolving conflicts in favor of `master` means that `nightly-testing` will rather break than silently undoing changes made on `master`. Co-authored-by: Joscha <joscha@plugh.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Resolving merge conflicts in favor of
nightly-testingwhen mergingmastermay be convenient for nightly maintainers, but it can lead to changes made onmasteraccidentally being dropped again later in the bump PR. For an example case, see #40189 (see #PR reviews > #39443 `nonempty_preimage_iff` @ 💬 for an explanation of what happened).Resolving conflicts in favor of
mastermeans thatnightly-testingwill rather break than silently undoing changes made onmaster.