lib/Tools/make
author wenzelm
Fri Oct 08 15:03:38 1999 +0200 (1999-10-08)
changeset 7795 111d2a65e1c6
parent 3007 e5efa177ee0c
child 9788 df671fa2562a
permissions -rwxr-xr-x
tuned usage;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2437
     2
#
wenzelm@2437
     3
# $Id$
wenzelm@2437
     4
#
wenzelm@2437
     5
# DESCRIPTION: Isabelle make utility
wenzelm@2437
     6
wenzelm@2437
     7
wenzelm@2437
     8
PRG=$(basename $0)
wenzelm@2437
     9
wenzelm@2437
    10
function usage()
wenzelm@2437
    11
{
wenzelm@2437
    12
  echo
wenzelm@2437
    13
  echo "Usage: $PRG [ARGS ...]"
wenzelm@2437
    14
  echo
wenzelm@7795
    15
  echo "  Compile the logic in current directory using IsaMakefile."
wenzelm@2437
    16
  echo "  ARGS are directly passed to the system make program."
wenzelm@2437
    17
  echo
wenzelm@2437
    18
  exit 1
wenzelm@2437
    19
}
wenzelm@2437
    20
wenzelm@2437
    21
wenzelm@2437
    22
## main
wenzelm@2437
    23
wenzelm@2437
    24
[ "$1" = "-?" ] && usage
wenzelm@2437
    25
wenzelm@2437
    26
exec make -f IsaMakefile "$@"