Allow symlinks to shell scripts
authorgagern
Wed Apr 20 14:18:33 2005 +0200 (2005-04-20)
changeset 1577898af3693f6b3
parent 15777 311aedc96e71
child 15779 aed221aff642
Allow symlinks to shell scripts
NEWS
bin/isabelle
bin/isabelle-interface
bin/isabelle-process
     1.1 --- a/NEWS	Wed Apr 20 00:45:54 2005 +0200
     1.2 +++ b/NEWS	Wed Apr 20 14:18:33 2005 +0200
     1.3 @@ -344,6 +344,9 @@
     1.4  * isatool usedir: option -f allows specification of the ML file to be
     1.5    used by Isabelle; default is ROOT.ML.
     1.6  
     1.7 +* symlinks to Isabelle, isabelle, isabelle-interface and isabelle-process
     1.8 +  are allowed; isabelle directories are determined based on link target.
     1.9 +
    1.10  * ISABELLE_DOC_FORMAT setting specifies preferred document format (for
    1.11    isatool doc, isatool mkdir, display_drafts etc.).
    1.12  
     2.1 --- a/bin/isabelle	Wed Apr 20 00:45:54 2005 +0200
     2.2 +++ b/bin/isabelle	Wed Apr 20 14:18:33 2005 +0200
     2.3 @@ -5,7 +5,11 @@
     2.4  #
     2.5  # Smart selection of isabelle-process versus isabelle-interface.
     2.6  
     2.7 -THIS=$(cd "$(dirname "$0")"; pwd)
     2.8 +THIS="$0"
     2.9 +while [ -L "$THIS" ]; do
    2.10 +    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    2.11 +done
    2.12 +THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
    2.13  NAME="$(basename "$0")"
    2.14  
    2.15  case "$NAME" in
     3.1 --- a/bin/isabelle-interface	Wed Apr 20 00:45:54 2005 +0200
     3.2 +++ b/bin/isabelle-interface	Wed Apr 20 14:18:33 2005 +0200
     3.3 @@ -10,7 +10,11 @@
     3.4  
     3.5  PRG="$(basename "$0")"
     3.6  
     3.7 -ISABELLE_HOME="$(dirname "$0")/.."
     3.8 +THIS="$0"
     3.9 +while [ -L "$THIS" ]; do
    3.10 +    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    3.11 +done
    3.12 +ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
    3.13  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    3.14    { echo "$PRG probably not called from its original place!"; exit 2; }
    3.15  
     4.1 --- a/bin/isabelle-process	Wed Apr 20 00:45:54 2005 +0200
     4.2 +++ b/bin/isabelle-process	Wed Apr 20 14:18:33 2005 +0200
     4.3 @@ -10,7 +10,11 @@
     4.4  
     4.5  PRG="$(basename "$0")"
     4.6  
     4.7 -ISABELLE_HOME="$(dirname "$0")/.."
     4.8 +THIS="$0"
     4.9 +while [ -L "$THIS" ]; do
    4.10 +    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    4.11 +done
    4.12 +ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
    4.13  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    4.14    { echo "$PRG probably not called from its original place!"; exit 2; }
    4.15