lib/Tools/testdir

Deleted a useless definition

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