Rename remove_error and include_error to remove_failed and include_failed #361

	name: Label PR

	on:
	pull_request_target:
	types:
	- opened
	- reopened
	- edited

	jobs:
	label:
	name: Label PR
	runs-on: ubuntu-latest
	permissions:
	pull-requests: write
	steps:
	- run: \|
	export LABELS=$(gh repo view $REPO --json="labels" --jq='.labels[].name \| select(startswith(env.PREFIX))')
	python <(cat <<EOF
	import sys, os
	from urllib.parse import quote
	url = f"https://github.com/{os.environ['REPO']}/labels/"
	labels = os.environ['LABELS'].strip().splitlines()
	prefix = os.environ['PREFIX']
	checked = "- [x] "
	unchecked = "- [ ] "
	for line in os.environ["BODY"].splitlines():
	for label in labels:
	if label.startswith(prefix) and line.strip().endswith(url + quote(label)):
	if line.strip().startswith(checked):
	print(f"--add-label={label}")
	elif line.strip().startswith(unchecked):
	print(f"--remove-label={label}")
	EOF
	) \| xargs --no-run-if-empty --delimiter '\n' gh pr --repo $REPO edit $NUMBER

	env:
	PREFIX: "PR type: "
	REPO: procrastinate-org/procrastinate
	BODY: ${{github.event.pull_request.body}}
	NUMBER: ${{ github.event.pull_request.number }}
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

Provide feedback