author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 2477 | ff44d0e1953a |
permissions | -rwxr-xr-x |
#!/bin/bash -norc # # $Id$ # # DESCRIPTION: use dir without committing into database PRG=$(basename $0) function usage() { echo echo "Usage: $PRG LOGIC DIR" echo echo " Use dir without committing into database (FIXME ISABELLE_HTML)." echo exit 1 } ## args [ $# -ne 2 ] && usage LOGIC="$1"; shift DIR="$1"; shift ## main exec $ISABELLE \ -e "make_html := $ISABELLE_HTML;" \ -e "exit_use_dir\"$DIR\"; quit();" \ -rq $LOGIC