Skip to content

Move CGAL issue template and add config settings #1764

Move CGAL issue template and add config settings

Move CGAL issue template and add config settings #1764

Workflow file for this run

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 "[email protected]"
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