lib/scripts/getsettings
changeset 34255 2dd2547acb41
parent 34254 14f6df4f473d
child 34257 b5176fd9ab3c
equal deleted inserted replaced
34254:14f6df4f473d 34255:2dd2547acb41
    19 fi
    19 fi
    20 
    20 
    21 #key executables
    21 #key executables
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    23 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    23 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    24 #legacy settings
       
    25 ISABELLE="$ISABELLE_PROCESS"
       
    26 ISATOOL="$ISABELLE_TOOL"
       
    27 
    24 
    28 function isabelle-process ()
    25 function isabelle-process ()
    29 {
    26 {
    30   "$ISABELLE_PROCESS" "$@"
    27   "$ISABELLE_PROCESS" "$@"
    31 }
    28 }