# HG changeset patch
# User wenzelm
# Date 904218766 -7200
# Node ID 4325d853494ab11a1e0a1c46f2b57ef0e4a9ef8b
# Parent  8fc3828fdc8a206c7eb3319804883b7934705968
tuned;
added ISABELLE_USEDIR_OPTIONS;

diff -r 8fc3828fdc8a -r 4325d853494a build
--- a/build	Thu Aug 27 11:53:45 1998 +0200
+++ b/build	Thu Aug 27 13:52:46 1998 +0200
@@ -93,13 +93,16 @@
   echo
   echo "Please check $ISABELLE_HOME/etc/settings"
   [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
-  echo "to make sure that Isabelle's ML system settings are appropriate."
+  echo "to make sure that Isabelle's ML system settings and compilation options"
+  echo "are appropriate."
   echo
-  echo "Your current values are:"
+  echo "The current values are:"
   echo
   echo "  ML_SYSTEM=$ML_SYSTEM"
   echo "  ML_HOME=$ML_HOME"
   echo "  ML_OPTIONS=$ML_OPTIONS"
+  echo
+  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
 fi