removed redundant readlink call
authorgagern
Wed Apr 20 19:00:30 2005 +0200 (2005-04-20)
changeset 157843a214de33d53
parent 15783 82e40c9a0f3f
child 15785 ae6943098223
removed redundant readlink call
bin/isabelle
bin/isabelle-interface
bin/isabelle-process
     1.1 --- a/bin/isabelle	Wed Apr 20 18:57:05 2005 +0200
     1.2 +++ b/bin/isabelle	Wed Apr 20 19:00:30 2005 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  while [ -L "$THIS" ]; do
     1.5      THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
     1.6  done
     1.7 -THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
     1.8 +THIS="$(cd "$(dirname "$THIS")"; pwd)"
     1.9  NAME="$(basename "$0")"
    1.10  
    1.11  case "$NAME" in
     2.1 --- a/bin/isabelle-interface	Wed Apr 20 18:57:05 2005 +0200
     2.2 +++ b/bin/isabelle-interface	Wed Apr 20 19:00:30 2005 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  while [ -L "$THIS" ]; do
     2.5      THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
     2.6  done
     2.7 -ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
     2.8 +ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
     2.9  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    2.10    { echo "$PRG probably not called from its original place!"; exit 2; }
    2.11  
     3.1 --- a/bin/isabelle-process	Wed Apr 20 18:57:05 2005 +0200
     3.2 +++ b/bin/isabelle-process	Wed Apr 20 19:00:30 2005 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4  while [ -L "$THIS" ]; do
     3.5      THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
     3.6  done
     3.7 -ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
     3.8 +ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
     3.9  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    3.10    { echo "$PRG probably not called from its original place!"; exit 2; }
    3.11