lib/Tools/make
changeset 2501 632e126852fc
parent 2437 63249c1c544a
child 2593 012be3cc5203
equal deleted inserted replaced
2500:777c90aa20b2 2501:632e126852fc
    23 
    23 
    24 [ "$1" = "-?" ] && usage
    24 [ "$1" = "-?" ] && usage
    25 
    25 
    26 
    26 
    27 . $ISABELLE_HOME/lib/scripts/getplatform
    27 . $ISABELLE_HOME/lib/scripts/getplatform
    28 
       
    29 export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
    28 export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
    30 
    29 
    31 exec make -f IsaMakefile "$@"
    30 exec make -f IsaMakefile "$@"