Use default_random #1791

	name: Documentation Removal

	on:
	pull_request_target:
	types: [closed, removed, workflow_dispatch]
	permissions:
	contents: read

	jobs:
	build:

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

	steps:
	- uses: actions/checkout@v3
	- name: delete directory
	run: \|
	set -x
	git config --global user.email "cgal@geometryfactory.com"
	git config --global user.name "cgaltest"
	git clone https://CGAL:${{ secrets.PUSH_TO_CGAL_GITHUB_IO_TOKEN }}@github.com/CGAL/cgal.github.io.git
	PR_NUMBER=$(python -c "import json; import os; y = json.load(open(os.environ['GITHUB_EVENT_PATH'])); print(y[\"number\"])")
	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