chore: add comments in CI about || true (#8336)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Dec 15, 2023 · 7a8021e · 7a8021e
1 parent 35f15cb
commit 7a8021e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/.github/workflows/nightly_bump_toolchain.yml b/.github/workflows/nightly_bump_toolchain.yml
@@ -31,4 +31,4 @@ jobs:
         git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
         git add lean-toolchain
         git commit -m "chore: bump to ${RELEASE_TAG}"
-        git push origin nightly-testing || true
+        git push origin nightly-testing
diff --git a/.github/workflows/nightly_merge_master.yml b/.github/workflows/nightly_merge_master.yml
@@ -25,7 +25,9 @@ jobs:
       - name: Merge master to nightly favoring nightly changes
         run: |
           git checkout nightly-testing
+          # If the merge goes badly, we proceed anyway via '|| true'
+          # CI will report failures on the 'nightly-testing' branch direct to Zulip.
           git merge master --strategy-option ours --no-commit --allow-unrelated-histories || true
           git add .
           git commit -m "Merge master into nightly-testing"
-          git push origin nightly-testing || true
+          git push origin nightly-testing