# HG changeset patch
# User gagern
# Date 1113999513 -7200
# Node ID 98af3693f6b36f199807850a237f6e03c3b1e91a
# Parent  311aedc96e715970bf114f196c105ab981ea4675
Allow symlinks to shell scripts

diff -r 311aedc96e71 -r 98af3693f6b3 NEWS
--- a/NEWS	Wed Apr 20 00:45:54 2005 +0200
+++ b/NEWS	Wed Apr 20 14:18:33 2005 +0200
@@ -344,6 +344,9 @@
 * isatool usedir: option -f allows specification of the ML file to be
   used by Isabelle; default is ROOT.ML.
 
+* symlinks to Isabelle, isabelle, isabelle-interface and isabelle-process
+  are allowed; isabelle directories are determined based on link target.
+
 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for
   isatool doc, isatool mkdir, display_drafts etc.).
 
diff -r 311aedc96e71 -r 98af3693f6b3 bin/isabelle
--- a/bin/isabelle	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle	Wed Apr 20 14:18:33 2005 +0200
@@ -5,7 +5,11 @@
 #
 # Smart selection of isabelle-process versus isabelle-interface.
 
-THIS=$(cd "$(dirname "$0")"; pwd)
+THIS="$0"
+while [ -L "$THIS" ]; do
+    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
+done
+THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
 NAME="$(basename "$0")"
 
 case "$NAME" in
diff -r 311aedc96e71 -r 98af3693f6b3 bin/isabelle-interface
--- a/bin/isabelle-interface	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle-interface	Wed Apr 20 14:18:33 2005 +0200
@@ -10,7 +10,11 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
+THIS="$0"
+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/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
 
diff -r 311aedc96e71 -r 98af3693f6b3 bin/isabelle-process
--- a/bin/isabelle-process	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle-process	Wed Apr 20 14:18:33 2005 +0200
@@ -10,7 +10,11 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
+THIS="$0"
+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/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }