Skip to content

chore: rename List.modifyNth->modify and insertNth->insertIdx (#1003) #491

chore: rename List.modifyNth->modify and insertNth->insertIdx (#1003)

chore: rename List.modifyNth->modify and insertNth->insertIdx (#1003) #491

# This job merges every commit to `main` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`.
name: Merge main to nightly
on:
push:
branches:
- main
jobs:
merge-to-nightly:
if: github.repository_owner == 'leanprover-community'
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
fetch-depth: 0
token: ${{ secrets.NIGHTLY_TESTING }}
- name: Configure Git User
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
- name: Merge main to nightly favoring nightly changes
run: |
git checkout nightly-testing
git merge main --strategy-option ours --no-commit --allow-unrelated-histories
git commit -m "Merge main into nightly-testing"
git push origin nightly-testing