diff -r dae7f8ca5001 -r ff44d0e1953a lib/Tools/testdir
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/testdir	Tue Jan 07 09:05:26 1997 +0100
@@ -0,0 +1,34 @@
+#!/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