lib/scripts/configure

--- a/lib/scripts/configure	Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/bin/sh
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# configure - adapt Isabelle distribution to system environment
-
-## patch scripts
-
-cd "`dirname "$0"`"
-
-if bash -c :
-then
-  bash lib/scripts/patch-scripts.bash
-else
-  echo "FATAL ERROR: bash not found!"
-  exit 2
-fi