even more robust and user friendly invocation (no longer requieres
authorwenzelm
Thu Mar 06 12:28:17 1997 +0100 (1997-03-06)
changeset 273529434f9b95dd
parent 2734 e9bbef1b2fbe
child 2736 476adc742599
even more robust and user friendly invocation (no longer requieres
absolute path names);
bin/isabelle
bin/isatool
     1.1 --- a/bin/isabelle	Wed Mar 05 17:15:31 1997 +0100
     1.2 +++ b/bin/isabelle	Thu Mar 06 12:28:17 1997 +0100
     1.3 @@ -9,21 +9,9 @@
     1.4  
     1.5  PRG=$(basename $0)
     1.6  
     1.7 -ISABELLE_HOME=$(dirname $(dirname $0))
     1.8 -case "$ISABELLE_HOME" in
     1.9 -  /*)
    1.10 -    if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
    1.11 -      . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
    1.12 -    else
    1.13 -      echo "ERROR: $PRG probably not called from its original place!"
    1.14 -      exit 1
    1.15 -    fi
    1.16 -    ;;
    1.17 -  *)
    1.18 -    echo "ERROR: $PRG not called with absolute path specification!"
    1.19 -    exit 1
    1.20 -    ;;
    1.21 -esac
    1.22 +ISABELLE_HOME=$(dirname $0)/..
    1.23 +. $ISABELLE_HOME/lib/scripts/getsettings || \
    1.24 +  { echo "$PRG probably not called from its original place!"; exit 2 }
    1.25  
    1.26  
    1.27  ## diagnostics
     2.1 --- a/bin/isatool	Wed Mar 05 17:15:31 1997 +0100
     2.2 +++ b/bin/isatool	Thu Mar 06 12:28:17 1997 +0100
     2.3 @@ -1,29 +1,18 @@
     2.4 -#!/bin/bash -norc
     2.5 +#!/bin/bash -x
     2.6  #
     2.7  # $Id$
     2.8  #
     2.9 -# Isabelle tool starter -- keeps your PATH name space clean.
    2.10 +# Isabelle tool starter -- provides settings environment,
    2.11 +#   also keeps your PATH name space clean.
    2.12  
    2.13  
    2.14  ## settings
    2.15  
    2.16  PRG=$(basename $0)
    2.17  
    2.18 -ISABELLE_HOME=$(dirname $(dirname $0))
    2.19 -case "$ISABELLE_HOME" in
    2.20 -  /*)
    2.21 -    if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then
    2.22 -      . $ISABELLE_HOME/lib/scripts/getsettings || exit 2
    2.23 -    else
    2.24 -      echo "ERROR: $PRG probably not called from its original place!"
    2.25 -      exit 1
    2.26 -    fi
    2.27 -    ;;
    2.28 -  *)
    2.29 -    echo "ERROR: $PRG not called with absolute path specification!"
    2.30 -    exit 1
    2.31 -    ;;
    2.32 -esac
    2.33 +ISABELLE_HOME=$(dirname $0)/..
    2.34 +. $ISABELLE_HOME/lib/scripts/getsettings || \
    2.35 +  { echo "$PRG probably not called from its original place!"; exit 2 }
    2.36  
    2.37  
    2.38  ## diagnostics