Bash scripts: /usr/bin/env bash rather than /bin/bash

parent b0c6979f
Pipeline #161635709 passed with stages
in 48 minutes and 28 seconds
#! /bin/bash
#! /usr/bin/env bash
set -e
......
#!/bin/bash
#! /usr/bin/env bash
script_dir=$(cd "$(dirname "$0")" && pwd -P)
src_dir="$(dirname "$script_dir")"
......
#! /bin/bash
#! /usr/bin/env bash
set -e
......
#!/bin/bash
#! /usr/bin/env bash
# plots the output of 'dune build @runtest_locator'
......
#!/bin/bash
#! /usr/bin/env bash
# run test at most NUM times, exit at first failure
if [ $# -ne 2 ] || [ "$1" -le 0 ] || [ ! -f $2 ]; then
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment