diff options
| author | Théo Zimmermann | 2017-11-29 15:45:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-11-29 15:46:17 +0100 |
| commit | 8cd635c99ae95f5d545b17df608e8276b9b5c93c (patch) | |
| tree | e32c0f058ddb2c0afd5d49d5faef9bb7ebbab065 /dev/tools | |
| parent | bc1fb4be47578b4da554aef69150acd77e82aba1 (diff) | |
This script apparently uses bash-specific features.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 63c42629cd..0c4a79bfd3 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -1,4 +1,6 @@ -#!/bin/sh -e +#!/usr/bin/env bash + +set -e # This script depends (at least) on git and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ |