# HG changeset patch
# User berghofe
# Date 1106825720 -3600
# Node ID 6e60be6a6c210450d95ba264f5ef798d8c6a844b
# Parent  24132e4965612ed7b53005bc7f1319b49fd82bcb
Proofs are now hidden by default.

diff -r 24132e496561 -r 6e60be6a6c21 lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Jan 27 12:34:52 2005 +0100
+++ b/lib/Tools/usedir	Thu Jan 27 12:35:20 2005 +0100
@@ -17,7 +17,7 @@
   echo
   echo "  Options are:"
   echo "    -D PATH      dump generated document sources into PATH"
-  echo "    -H BOOL      hide proofs and some other commands in document (default false)"
+  echo "    -H BOOL      hide proofs and some other commands in document (default true)"
   echo "    -P PATH      set path for remote theory browsing information"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -c BOOL      tell ML system to compress output image (default true)"
@@ -65,7 +65,7 @@
 BUILD=""
 COMPRESS=true
 DOCUMENT=false
-HIDE=false
+HIDE=true
 ROOT_FILE=ROOT.ML
 DOCUMENT_GRAPH=false
 INFO=false