bin/isabelle-process
changeset 15778 98af3693f6b3
parent 14981 e73f8140af78
child 15779 aed221aff642
equal deleted inserted replaced
15777:311aedc96e71 15778:98af3693f6b3
     8 
     8 
     9 ## settings
     9 ## settings
    10 
    10 
    11 PRG="$(basename "$0")"
    11 PRG="$(basename "$0")"
    12 
    12 
    13 ISABELLE_HOME="$(dirname "$0")/.."
    13 THIS="$0"
       
    14 while [ -L "$THIS" ]; do
       
    15     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
       
    16 done
       
    17 ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
    14 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    18 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    15   { echo "$PRG probably not called from its original place!"; exit 2; }
    19   { echo "$PRG probably not called from its original place!"; exit 2; }
    16 
    20 
    17 
    21 
    18 ## diagnostics
    22 ## diagnostics