# HG changeset patch
# User wenzelm
# Date 1192111049 -7200
# Node ID 50959112a4e1018e8ef624af3fec7fe991b30148
# Parent  4992239a414ecc5ad13f4eb2158bccdd1538c16a
usage: HOL_USEDIR_OPTIONS;

diff -r 4992239a414e -r 50959112a4e1 lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Oct 11 10:23:09 2007 +0200
+++ b/lib/Tools/usedir	Thu Oct 11 15:57:29 2007 +0200
@@ -38,6 +38,7 @@
   echo "  information (HTML etc.) according to settings."
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
   exit 1
 }