lib/Tools/make
author wenzelm
Thu Jan 09 16:44:57 1997 +0100 (1997-01-09)
changeset 2501 632e126852fc
parent 2437 63249c1c544a
child 2593 012be3cc5203
permissions -rwxr-xr-x
*** empty log message ***
     1 #!/bin/bash -norc
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: Isabelle make utility
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [ARGS ...]"
    14   echo
    15   echo "  Compiles logic in current directory using IsaMakefile."
    16   echo "  ARGS are directly passed to the system make program."
    17   echo
    18   exit 1
    19 }
    20 
    21 
    22 ## main
    23 
    24 [ "$1" = "-?" ] && usage
    25 
    26 
    27 . $ISABELLE_HOME/lib/scripts/getplatform
    28 export ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
    29 
    30 exec make -f IsaMakefile "$@"