[Merged by Bors] - chore(CI): fix merge conflict resolution for nightly-testing

.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