diff --git a/comptime.sh b/comptime.sh index 71c5f08a..d5ef7271 100755 --- a/comptime.sh +++ b/comptime.sh @@ -1,4 +1,4 @@ -#!/bin/sh -e +#!/bin/bash -e path="." if [ x"$1" != x ]; then path="$1"