# HG changeset patch
# User wenzelm
# Date 1127329287 -7200
# Node ID 3be0d6cfbc3a080473ac493b7db5f93dba998e12
# Parent  c45677c1aea0f8f193b238dc311e79ef1b6173bb
echo HOL_USEDIR_OPTIONS;

diff -r c45677c1aea0 -r 3be0d6cfbc3a build
--- a/build	Wed Sep 21 21:00:57 2005 +0200
+++ b/build	Wed Sep 21 21:01:27 2005 +0200
@@ -119,6 +119,7 @@
   echo "  ML_PLATFORM=$ML_PLATFORM"
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
 fi