diff -r fb8c5a66dbe8 -r df671fa2562a lib/Tools/getenv --- a/lib/Tools/getenv Fri Sep 01 17:48:31 2000 +0200 +++ b/lib/Tools/getenv Fri Sep 01 17:50:36 2000 +0200 @@ -1,13 +1,15 @@ #!/bin/bash # # $Id$ +# Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) # # DESCRIPTION: get values from Isabelle settings environment ## diagnostics -PRG=$(basename $0) +PRG=$(basename "$0") function usage() { @@ -51,7 +53,7 @@ # args -[ -n "$ALL" -a $# -ne 0 ] && usage +[ -n "$ALL" -a "$#" -ne 0 ] && usage ## main @@ -59,7 +61,7 @@ if [ -n "$ALL" ]; then env | sort else - for VAR in $* + for VAR in "$@" do if [ -n "$BASE" ]; then eval "echo \$$VAR"