mirror of https://github.com/CGAL/cgal
37 lines
1.2 KiB
YAML
37 lines
1.2 KiB
YAML
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
|