diff --git a/.github/workflows/nightly_merge_master.yml b/.github/workflows/nightly_merge_master.yml index 097518d25dcf5a..e371f9e9b4cd10 100644 --- a/.github/workflows/nightly_merge_master.yml +++ b/.github/workflows/nightly_merge_master.yml @@ -1,4 +1,4 @@ -# This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`. +# This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `master`. name: Merge master to nightly @@ -49,15 +49,17 @@ jobs: git config user.name "mathlib-nightly-testing[bot]" git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com" - - name: Merge master to nightly favoring nightly changes + - name: Merge master to nightly favoring master changes run: | cd nightly-testing git remote add upstream https://github.com/leanprover-community/mathlib4.git git fetch upstream master - # Merge master into nightly-testing, resolving conflicts in favor of nightly-testing + # Merge master into nightly-testing, resolving conflicts in favor of master. + # In the past, we've silently dropped changes made on master because + # conflicts were resolved in favor of nightly-testing, which is bad. # If the merge goes badly, we proceed anyway via '|| true'. # CI will report failures on the 'nightly-testing' branch direct to Zulip. - git merge upstream/master --strategy-option ours --no-commit --allow-unrelated-histories || true + git merge upstream/master --strategy-option theirs --no-commit --allow-unrelated-histories || true # We aggressively run `lake update`, to avoid having to do this by hand. # When Batteries changes break Mathlib, this will likely show up on nightly-testing first. lake update -v