Logger widget panel #16
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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 |