Run full tests #13

	name: Run full tests
	on:
	schedule:
	- cron: '0 1 * * 6'
	workflow_dispatch:
	jobs:
	run:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v3
	- run: \|
	set -x
	git fetch
	if gh pr checkout full-tests
	then
	gh pr close --comment 'Recreating'
	git checkout master
	git branch -D full-tests
	git push origin :full-tests
	git reset --hard master
	fi
	git checkout -b full-tests
	# GitHub apparently does not let you create a PR with no commits:
	git config --global user.email git@example.org
	git config --global user.name run-full-test
	git commit --allow-empty --message 'Phony commit'
	git push origin full-tests
	# Not using --draft to ensure notifications are sent:
	gh pr create --head full-tests --title 'Testing master (do not merge)' --body 'Close this PR if it passes; otherwise please fix failures.' --label full-test
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

Provide feedback