diff -r 2edc5b01e5a7 -r 96234bf96bf9 configure
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/configure	Mon Feb 17 17:22:19 1997 +0100
@@ -0,0 +1,13 @@
+#!/bin/sh
+#
+# $Id$
+#
+# configure - adapt Isabelle distribution to system environment
+
+if bash -norc -c ""
+then
+  bash lib/scripts/patch-scripts.bash
+else
+  echo "FATAL ERROR: bash not found!"
+  exit 2
+fi