--- 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
--- 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; }
--- 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; }