--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/configure	Mon Jun 20 16:41:47 2005 +0200
@@ -0,0 +1,18 @@
+#!/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