mirror of https://github.com/CGAL/cgal
43 lines
1.4 KiB
YAML
43 lines
1.4 KiB
YAML
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 main
|
|
fi
|