update reuse to v5 #1784

	name: Documentation Removal

	on:
	workflow_dispatch:
	inputs:
	PR_NUMBER:
	description: 'Pull request number for which the documentation should be removed'
	type: number
	required: true
	pull_request_target:
	types: [closed]
	permissions:
	contents: read

	jobs:
	delete_doc:
	permissions:
	contents: write # for Git to git push
	runs-on: ubuntu-latest

	steps:
	- uses: actions/checkout@v4
	- name: delete directory ${{ github.event.inputs.PR_NUMBER \|\| github.event.pull_request.number }}/ in cgal.github.io
	env:
	PR_NUMBER: ${{ github.event.inputs.PR_NUMBER \|\| github.event.pull_request.number }}
	run: \|
	set -x
	git config --global user.email "[email protected]"
	git config --global user.name "cgaltest"
	git clone https://CGAL:${{ secrets.PUSH_TO_CGAL_GITHUB_IO_TOKEN }}@github.com/CGAL/cgal.github.io.git
	cd cgal.github.io/
	egrep -v " ${PR_NUMBER}\." index.html > tmp.html \|\| true
	if [ -n "$(diff -q ./index.html ./tmp.html)" ]; then
	mv tmp.html index.html
	fi
	if [ -d ${PR_NUMBER} ]; then
	git rm -r ${PR_NUMBER}
	fi
	# `git diff --quiet` exits with 1 if there is a diff
	if ! git diff --quiet; then
	git commit -a --amend -m"base commit" && git push -f -u origin master
	fi

Provide feedback