diff options
Diffstat (limited to 'tools/generate_patch_from_jenkins.sh')
| -rwxr-xr-x | tools/generate_patch_from_jenkins.sh | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tools/generate_patch_from_jenkins.sh b/tools/generate_patch_from_jenkins.sh deleted file mode 100755 index 0965015cc..000000000 --- a/tools/generate_patch_from_jenkins.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/usr/bin/env bash -set -euo pipefail - -PATCH=$(git diff | base64 -w 0) -if [ -n "$PATCH" ]; then - echo "Jenkins made some fixes to your PR. To apply these changes to your working directory," - echo "copy and run the following command (triple-click to select the entire line):" - echo - echo "echo -n $PATCH | base64 -d | git apply -" - echo -fi |