Merge pull request 'here it is' (#101) from develop-1001 into master

Reviewed-on: #101

.gitea/workflows/pr-closed.yml

@@ -20,12 +20,26 @@ jobs:
           echo env: ${{ env.GITHUB_HEAD_REF }}
           echo env: ${{ env.GITHUB_BASE_REF }}
       - name: delete develop branch
+        id: delete_develop_branch
         run: git push origin --delete ${{ github.head_ref }}
+        continue-on-error: true
+      - uses: mainmatter/continue-on-error-comment@v1
+        with:
+          repo-token: ${{ secrets.TEA_TOKEN }}
+          outcome: ${{ steps.delete_develop_branch.outcome }}
+          test-id: Error code ${{ matrix.code }}
       - name: get build branch name
         run: |
           firstString=${{ github.head_ref }}
           secondString="build-"
           echo ::set-env name=BUILD_BRANCH::${firstString/develop-/"$secondString"}
       - name: delete build branch
+        id: delete_build_branch
         run: git push origin --delete ${{ env.BUILD_BRANCH }}
+        continue-on-error: true
+      - uses: mainmatter/continue-on-error-comment@v1
+        with:
+          repo-token: ${{ secrets.TEA_TOKEN }}
+          outcome: ${{ steps.delete_build_branch.outcome }}
+          test-id: Error code ${{ matrix.code }}