Skip to content

Logger Widget 2 (based on #2700) #799

Logger Widget 2 (based on #2700)

Logger Widget 2 (based on #2700) #799

Workflow file for this run

# For more information about TARDIS pipelines, please refer to:
#
# https://tardis-sn.github.io/tardis/contributing/development/continuous_integration.html
name: clean-docs
on:
delete:
branches: # remove deleted branches
- "*"
pull_request_target: # remove closed or merged pull requests
branches:
- "*"
types:
- closed
env:
DEPLOY_BRANCH: gh-pages # deployed docs branch
jobs:
clean:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Set folder to delete
run: |
if [[ $EVENT == delete ]]; then
echo "DEST_DIR=$EVENT_TYPE/$EVENT_REF" >> $GITHUB_ENV
elif [[ $EVENT == pull_request_target ]]; then
echo "DEST_DIR=pull/$PR" >> $GITHUB_ENV
else
echo "Unexpected event trigger $EVENT"
exit 1
fi
cat $GITHUB_ENV
env:
PR: ${{ github.event.number }}
EVENT: ${{ github.event_name }}
EVENT_REF: ${{ github.event.ref }}
EVENT_TYPE: ${{ github.event.ref_type }}
- name: Clean ${{ env.DEST_DIR }}
run: |
git fetch origin ${{ env.DEPLOY_BRANCH }}
git checkout ${{ env.DEPLOY_BRANCH }}
git config user.name "TARDIS Bot"
git config user.email tardis.sn.bot@gmail.com
if [[ -d $DEST_DIR ]]; then
git rm -rf $DEST_DIR
git commit -m "clean $DEST_DIR"
git push
else
echo "$DEST_DIR does not exist"
fi