jenkins.sh: use sh instead of bash

Change-Id: Ia65e960dc7d74e6bb7a2463316d09622e9788c97 Suggested-by: msuraev
2016-10-17 18:00:42 +02:00 · 2016-10-17 18:00:42 +02:00 · 4079b4a976
parent 722c2fd579
commit 4079b4a976
1 changed files with 1 additions and 1 deletions
--- a/contrib/jenkins.sh
+++ b/contrib/jenkins.sh
@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh

 set -ex