# HG changeset patch
# User wenzelm
# Date 857731726 -3600
# Node ID 59bd96046ad6c1c7b22f7134c683ae5fc80376f3
# Parent  bcde71e5f3714318323cbb768d954575cfa732cc
moved settings comment to build;

diff -r bcde71e5f371 -r 59bd96046ad6 configure
--- 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