lib/Tools/usedir
changeset 34238 b28be884edda
parent 33830 1b634d37aa64
child 34261 8e36b3ac6083
     1.1 --- a/lib/Tools/usedir	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/lib/Tools/usedir	Mon Jan 04 11:55:23 2010 +0100
     1.3 @@ -38,7 +38,6 @@
     1.4    echo "  information (HTML etc.) according to settings."
     1.5    echo
     1.6    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
     1.7 -  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
     1.8    echo
     1.9    echo "  ML_PLATFORM=$ML_PLATFORM"
    1.10    echo "  ML_HOME=$ML_HOME"