lib/Tools/testdir
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2477 ff44d0e1953a
permissions -rwxr-xr-x
moved settings comment to build;

#!/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