delete_doc.yml

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@v4
    - 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