diff options
| -rwxr-xr-x | launch/launch | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/launch/launch b/launch/launch index b8757e6..050f522 100755 --- a/launch/launch +++ b/launch/launch @@ -1,4 +1,5 @@ #!/bin/sh +awk=awk me() { basename "$0"; } printhelp() { @@ -20,8 +21,20 @@ Config Syntax: HELPDOC } +# Make sure user is using GNU Awk (gawk) +checkawk() { + if ! ($awk -V >/dev/null 2>/dev/null && $awk -V | grep "GNU Awk" >/dev/null); then + if command -v gawk > /dev/null; then + awk=gawk + else + echo "$(me) requires GNU Awk (gawk) to function properly. Please install GNU Awk and try again." + exit 0 + fi + fi +} + gencache() { -awk ' +$awk ' BEGIN { print "run=\"$1\"; shift" print "case \"$run\" in" @@ -89,6 +102,7 @@ cache=$cachedir/cache [ $conf -nt $cache ] && gencache # Command line options +checkawk case "$1" in -g|--gen-cache) echo "Generating new cache: $cache"; gencache && cat $cache ;; -h|--help|'') printhelp ;; |