# HG changeset patch
# User wenzelm
# Date 936375414 -7200
# Node ID 94ae093f67063a25da49909ca174074f531b396c
# Parent  b1b2fbc375e216978b2d70e75ef2da8d4e7d850d
usage: tell ISABELLE_USEDIR_OPTIONS;

diff -r b1b2fbc375e2 -r 94ae093f6706 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Sep 03 18:16:02 1999 +0200
+++ b/lib/Tools/usedir	Fri Sep 03 18:16:54 1999 +0200
@@ -26,6 +26,8 @@
   echo "  Build object-logic or run examples. Also creates browsing"
   echo "  information (HTML etc.) according to settings."
   echo
+  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+  echo
   exit 1
 }