Delete docs for closed PRs #4

	name: Delete docs for closed PRs
	on:
	workflow_dispatch:
	schedule:
	- cron: 0 0 * * 0 # weekly

	# Sets permissions of the GITHUB_TOKEN to allow modification of contents
	permissions:
	contents: write

	jobs:
	remove_prs:
	runs-on: ubuntu-latest
	steps:
	# Checkout repo
	- uses: actions/checkout@v4
	- name: Set up Python
	uses: actions/setup-python@v4
	with:
	python-version: 3.12
	- name: Install requirements
	run: \|
	sudo apt-get install -y jq curl
	pip install -r requirements.txt
	curl https://raw.githubusercontent.com/newren/git-filter-repo/main/git-filter-repo -o ../git-filter-repo.py
	- name: Remove PRs
	# necessary to stop a creation of __pycache__/*pyc when running this script
	run: PYTHONDONTWRITEBYTECODE=1 python scripts/remove_closed_prs.py -g --cmd "python ../git-filter-repo.py"
	- name: Push back to origin
	shell: bash
	run: \|
	# if git remote -v doesn't return anything, then we ran the above script
	# (because git filter-repo removes the origin remote) and thus we should
	# push back to origin. If git remote -v returns something, there's
	# nothing to do.
	if [[ -z $(git remote -v) ]]; then
	git remote add origin https://github.com/plenoptic-org/plenoptic-documentation
	git push -f origin main
	fi

Provide feedback