chore: still fixing Mathlib CI #568

	name: add PR to changelog

	on:
	# needs read/write GH token, do not execute arbitrary code from PR
	pull_request_target:
	types: [closed]

	jobs:
	update-changelog:
	if: \|
	github.event.pull_request.merged == true &&
	contains(github.event.pull_request.labels.*.name, 'changelog') &&
	github.base_ref == 'master'
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v3
	with:
	# needs sufficiently elevated token to override branch protection rules
	token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
	- name: Update changelog
	run: \|
	set -euxo pipefail
	escaped_link=$(sed -e 's/[\/&]/\\&/g' <<'EOF'
	[${{ github.event.pull_request.title}}](${{ github.event.pull_request.html_url }})
	EOF
	)
	# insert link below first dashes line (https://stackoverflow.com/a/9453461/161659)
	sed -i "0,/^---/s/^---/\0\n\n* $escaped_link./" RELEASES.md
	# commit as github-actions bot (https://github.com/orgs/community/discussions/26560#discussioncomment-3252339)
	git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
	git config user.name "github-actions[bot]"
	git commit -i RELEASES.md -m "doc: update changelog"
	git push

Provide feedback