39 lines
1.3 KiB
YAML
39 lines
1.3 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/
|
|
sed -i "\@https://cgal.github.io/${PR_NUMBER}/@ d" index.html
|
|
git add index.html
|
|
git rm -r "${PR_NUMBER}/" || true
|
|
# `git diff --quiet` exits with 1 if there is a diff
|
|
if ! git diff --staged --quiet; then
|
|
git commit -a --amend -m"sole commit" && git push -f -u origin master
|
|
fi
|