delete_doc.yml

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 "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
         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