1.1 --- a/build	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/build	Mon Jan 04 11:55:23 2010 +0100
     1.3 @@ -119,7 +119,6 @@
     1.4    echo "  ML_PLATFORM=$ML_PLATFORM"
     1.5    echo
     1.6    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
     1.7 -  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
     1.8  fi
     1.9  
    1.10  
    1.11 @@ -162,7 +161,6 @@
    1.12    echo "ML_PLATFORM=$ML_PLATFORM"
    1.13    echo
    1.14    echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    1.15 -  echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
    1.16    echo
    1.17  fi
    1.18