# HG changeset patch
# User wenzelm
# Date 904229695 -7200
# Node ID 7299e531d4813d833b1a3abd9364cfc2f1a345fa
# Parent  a98dfbb19c8020b1c12a985d2ca3273e8306b134
fixed ISABELLE_USEDIR_OPTIONS;

diff -r a98dfbb19c80 -r 7299e531d481 build
--- a/build	Thu Aug 27 16:41:22 1998 +0200
+++ b/build	Thu Aug 27 16:54:55 1998 +0200
@@ -141,6 +141,8 @@
   echo "ML_HOME=$ML_HOME"
   echo "ML_OPTIONS=$ML_OPTIONS"
   echo
+  echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+  echo
 fi