chore: revert merging of #1736 (#1749) #790

	# 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: Generate app token
	id: app-token
	uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
	with:
	app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
	private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
	# The create-github-app-token README states that this token is masked and will not be logged accidentally.

	- name: Checkout repository
	uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
	with:
	fetch-depth: 0
	token: ${{ steps.app-token.outputs.token }}

	- name: Configure Git User
	run: \|
	git config user.name "mathlib-nightly-testing[bot]"
	git config user.email "mathlib-nightly-testing[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

Provide feedback