--- 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