diff options
| author | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2020-11-28 23:15:47 +0100 |
|---|---|---|
| committer | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2020-11-28 23:51:55 +0100 |
| commit | f120489c57fc84ed01fdb0cb47392e1f7ca597d3 (patch) | |
| tree | bd4c661d07f72921833cd400c9fd7e92d641461e /.github/workflows | |
| parent | bc9d7a47eaab965d4367a0ce0278acb9c534bbe0 (diff) | |
GitHub Actions: Upload patch artifact
Diffstat (limited to '.github/workflows')
| -rw-r--r-- | .github/workflows/pre-commit.yml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/.github/workflows/pre-commit.yml b/.github/workflows/pre-commit.yml index 1d62f305ed..87e7b66f1c 100644 --- a/.github/workflows/pre-commit.yml +++ b/.github/workflows/pre-commit.yml @@ -38,3 +38,18 @@ jobs: # HEAD is the not yet integrated PR merge commit +refs/pull/xxxx/merge # HEAD^1 is the PR target branch and HEAD^2 is the HEAD of the source branch extra_args: --from-ref HEAD^1 --to-ref HEAD + + - name: "Generate patch file" + if: failure() + run: | + git diff-index -p HEAD > "${PATCH_FILE}" + [ -s "${PATCH_FILE}" ] && echo "UPLOAD_PATCH_FILE=${PATCH_FILE}" >> "${GITHUB_ENV}" + env: + PATCH_FILE: pre-commit.patch + + - name: "Upload patch artifact" + if: failure() && env.UPLOAD_PATCH_FILE != null + uses: actions/upload-artifact@v2 + with: + name: ${{ env.UPLOAD_PATCH_FILE }} + path: ${{ env.UPLOAD_PATCH_FILE }} |