diff options
author | Brian Woods | 2019-10-07 18:25:53 -0700 |
---|---|---|
committer | Stefano Stabellini | 2019-10-21 15:24:09 -0700 |
commit | 5e87781c99ce3ffed0106ff3f7289ac04771f7c2 (patch) | |
tree | cde0e46439dab3ecd2480aed26802f2dffe1bcce /docker-extras | |
parent | 31ec364ae6ace3e6dc2c558bd3c386c76258c623 (diff) |
Change interpreter of disk_image to bash
disk_image has bashisms, change the interpreter to bash so it doesn't
get incorrectly interpreted if /bin/sh isn't bash.
Signed-off-by: Brian Woods <brian.woods@xilinx.com>
Reviewed-by: Stefano Stabellini <stefano.stabellini@xilinx.com>
Diffstat (limited to 'docker-extras')
-rwxr-xr-x | docker-extras/disk_image | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docker-extras/disk_image b/docker-extras/disk_image index 344c727..57b933f 100755 --- a/docker-extras/disk_image +++ b/docker-extras/disk_image @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # This helps to see what is going on set -e -x |