From 8cd635c99ae95f5d545b17df608e8276b9b5c93c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 29 Nov 2017 15:45:39 +0100
Subject: This script apparently uses bash-specific features.

---
 dev/tools/merge-pr.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

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/
-- 
cgit v1.2.3