| author | wenzelm |
| Thu, 27 Sep 2001 16:04:44 +0200 | |
| changeset 11590 | 14ae6a86813d |
| parent 10555 | 2323ec838401 |
| child 14981 | e73f8140af78 |
| permissions | -rwxr-xr-x |
#!/usr/bin/env bash # # $Id$ # Author: Markus Wenzel, TU Muenchen # License: GPL (GNU GENERAL PUBLIC LICENSE) # # 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 "$@"