# 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