| author | wenzelm | 
| Tue, 01 Aug 2000 00:19:07 +0200 | |
| changeset 9483 | 708a8a05497d | 
| parent 7795 | 111d2a65e1c6 | 
| child 9788 | df671fa2562a | 
| permissions | -rwxr-xr-x | 
#!/bin/bash # # $Id$ # # DESCRIPTION: Isabelle make utility PRG=$(basename $0) function usage() { echo echo "Usage: $PRG [ARGS ...]" echo echo " Compile the 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 "$@"