--- 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