# HG changeset patch
# User wenzelm
# Date 1119278507 -7200
# Node ID e1a36498a30f1c0e757318c4da01f2070ec18552
# Parent  baa008d0fee9e54ad90c0020ec88ad60428869f6
moved configure to lib/scripts;

diff -r baa008d0fee9 -r e1a36498a30f configure
--- 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
diff -r baa008d0fee9 -r e1a36498a30f lib/scripts/configure
--- /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