lib/scripts/getsettings
changeset 3118 24dae6222579
parent 2968 8ba30b031f31
child 3185 7a6c933d51d0
equal deleted inserted replaced
3117:74c1b51c1cd9 3118:24dae6222579
    21 
    21 
    22 #derived values
    22 #derived values
    23 ISABELLE=$ISABELLE_HOME/bin/isabelle
    23 ISABELLE=$ISABELLE_HOME/bin/isabelle
    24 ISATOOL=$ISABELLE_HOME/bin/isatool
    24 ISATOOL=$ISABELLE_HOME/bin/isatool
    25 
    25 
       
    26 #append ML system to paths
       
    27 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
       
    28 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
       
    29 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
       
    30 
    26 set +o allexport
    31 set +o allexport