diff -r ddb85eb8385f -r f7e4109e1725 lib/Tools/testdir
--- a/lib/Tools/testdir	Tue Apr 01 12:54:40 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/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