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 | |
| 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>
| -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 |