configure
changeset 2754 59bd96046ad6
parent 2655 9420efbb868e
child 3007 e5efa177ee0c
--- a/configure	Fri Mar 07 10:26:02 1997 +0100
+++ b/configure	Fri Mar 07 11:48:46 1997 +0100
@@ -13,14 +13,3 @@
   echo "FATAL ERROR: bash not found!"
   exit 2
 fi
-
-
-## manual steps
-
-PWD=`pwd`
-echo
-echo "***********************************************************"
-echo "* Please check the ML compiler settings in ./etc/settings *"
-echo "* before compiling Isabelle.                              *"
-echo "***********************************************************"
-echo