# HG changeset patch
# User wenzelm
# Date 939387827 -7200
# Node ID 624f609e10d7c90e7e6f1063372c5ec0a9158c18
# Parent  111d2a65e1c6bb9e12f01bf242b6ea1014a61b17
removed -c option;

diff -r 111d2a65e1c6 -r 624f609e10d7 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Oct 08 15:03:38 1999 +0200
+++ b/lib/Tools/usedir	Fri Oct 08 15:03:47 1999 +0200
@@ -17,7 +17,6 @@
   echo "  Options are:"
   echo "    -B           build mode with THIS_IS_ISABELLE_BUILD indication"
   echo "    -P PATH      set path for remote theory browsing information"
-  echo "    -c BOOL      clean document source after build (default true)"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
   echo "    -i BOOL      generate theory browsing information,"
@@ -39,7 +38,6 @@
 # options
 
 BUILD=""
-CLEANDOC=true
 DOCUMENT=false
 INFO=false
 RESET=false
@@ -60,9 +58,6 @@
       b)
         BUILD=true
         ;;
-      c)
-        CLEANDOC="$OPTARG"
-        ;;
       d)
         DOCUMENT="$OPTARG"
         ;;
@@ -134,9 +129,8 @@
 
 [ -z "$BUILD" ] && cd "$NAME"
 
-if [ "$DOCUMENT" != false -a -d document -a -f document/root.tex ]
-then DOC="$DOCUMENT"
-else DOC=""; fi
+DOC=""
+[ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT"
 
 
 SECONDS=0