moved configure to lib/scripts;

--- a/configure	Mon Jun 20 16:41:20 2005 +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

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