diff options
author | Makarius Wenzel <makarius@sketis.net> | 2000-09-02 20:06:01 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2000-09-02 20:06:01 +0000 |
commit | 4eae9ec679b594887cdb89625abdab70f2169578 (patch) | |
tree | aaad02f3359937c365192d9795d2c35345d468e4 | |
parent | b98a2d4a291aae264cbc36982667ef487171e0f7 (diff) |
more quoting;
-rw-r--r-- | isa/interface | 6 | ||||
-rw-r--r-- | isar/interface | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/isa/interface b/isa/interface index afd77142..3577fc39 100644 --- a/isa/interface +++ b/isa/interface @@ -7,7 +7,7 @@ ## diagnostics -PRG=$(basename $0) +PRG=$(basename "$0") function usage() { @@ -38,7 +38,7 @@ function fail() ## process command line -export PROOFGENERAL_HOME=$(cd $(dirname "$0"); cd ..; echo $PWD) +export PROOFGENERAL_HOME=$(cd $(dirname "$0"); cd ..; echo "$PWD") # options @@ -86,7 +86,7 @@ shift $(($OPTIND - 1)) # args FILES="$@" -shift $# +shift "$#" [ -z "$FILES" ] && FILES="Scratch.thy" diff --git a/isar/interface b/isar/interface index 544bad76..58f5a30c 100644 --- a/isar/interface +++ b/isar/interface @@ -7,7 +7,7 @@ ## diagnostics -PRG=$(basename $0) +PRG=$(basename "$0") function usage() { @@ -38,7 +38,7 @@ function fail() ## process command line -export PROOFGENERAL_HOME=$(cd $(dirname "$0"); cd ..; echo $PWD) +export PROOFGENERAL_HOME=$(cd $(dirname "$0"); cd ..; echo "$PWD") # options @@ -86,7 +86,7 @@ shift $(($OPTIND - 1)) # args FILES="$@" -shift $# +shift "$#" [ -z "$FILES" ] && FILES="Scratch.thy" |