author | wenzelm |
Fri, 04 Apr 1997 19:10:22 +0200 | |
changeset 2916 | d761a62da697 |
parent 2593 | 012be3cc5203 |
child 3007 | e5efa177ee0c |
permissions | -rwxr-xr-x |
#!/bin/bash -norc # # $Id$ # # DESCRIPTION: Isabelle make utility PRG=$(basename $0) function usage() { echo echo "Usage: $PRG [ARGS ...]" echo echo " Compiles logic in current directory using IsaMakefile." echo " ARGS are directly passed to the system make program." echo exit 1 } ## main [ "$1" = "-?" ] && usage exec make -f IsaMakefile "$@"