# HG changeset patch
# User wenzelm
# Date 856199523 -3600
# Node ID 9420efbb868e16f9b97094d660f2cc4fe22455f3
# Parent  6efa602921d1bf29bffffa9f84deef17a78a4b67
manual steps comment;

diff -r 6efa602921d1 -r 9420efbb868e configure
--- a/configure	Mon Feb 17 17:55:45 1997 +0100
+++ b/configure	Mon Feb 17 18:12:03 1997 +0100
@@ -4,6 +4,8 @@
 #
 # configure - adapt Isabelle distribution to system environment
 
+## patch scripts
+
 if bash -norc -c ""
 then
   bash lib/scripts/patch-scripts.bash
@@ -11,3 +13,14 @@
   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