# HG changeset patch
# User gagern
# Date 1114016430 -7200
# Node ID 3a214de33d53b78680a4bad1a4f32a7957933a6a
# Parent  82e40c9a0f3f10e238d95680020c2595cdb1f531
removed redundant readlink call

diff -r 82e40c9a0f3f -r 3a214de33d53 bin/isabelle
--- a/bin/isabelle	Wed Apr 20 18:57:05 2005 +0200
+++ b/bin/isabelle	Wed Apr 20 19:00:30 2005 +0200
@@ -9,7 +9,7 @@
 while [ -L "$THIS" ]; do
     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
 done
-THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
+THIS="$(cd "$(dirname "$THIS")"; pwd)"
 NAME="$(basename "$0")"
 
 case "$NAME" in
diff -r 82e40c9a0f3f -r 3a214de33d53 bin/isabelle-interface
--- a/bin/isabelle-interface	Wed Apr 20 18:57:05 2005 +0200
+++ b/bin/isabelle-interface	Wed Apr 20 19:00:30 2005 +0200
@@ -14,7 +14,7 @@
 while [ -L "$THIS" ]; do
     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
 done
-ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
+ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
 
diff -r 82e40c9a0f3f -r 3a214de33d53 bin/isabelle-process
--- a/bin/isabelle-process	Wed Apr 20 18:57:05 2005 +0200
+++ b/bin/isabelle-process	Wed Apr 20 19:00:30 2005 +0200
@@ -17,7 +17,7 @@
 while [ -L "$THIS" ]; do
     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
 done
-ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
+ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }