fixed ISABELLE_USEDIR_OPTIONS;
authorwenzelm
Thu Aug 27 16:54:55 1998 +0200 (1998-08-27)
changeset 53937299e531d481
parent 5392 a98dfbb19c80
child 5394 2049fbac1407
fixed ISABELLE_USEDIR_OPTIONS;
build
     1.1 --- a/build	Thu Aug 27 16:41:22 1998 +0200
     1.2 +++ b/build	Thu Aug 27 16:54:55 1998 +0200
     1.3 @@ -141,6 +141,8 @@
     1.4    echo "ML_HOME=$ML_HOME"
     1.5    echo "ML_OPTIONS=$ML_OPTIONS"
     1.6    echo
     1.7 +  echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
     1.8 +  echo
     1.9  fi
    1.10  
    1.11