Updated usage information for tool "usedir".
authorberghofe
Tue, 30 Sep 1997 17:29:32 +0200
changeset 3752 7ae403333ec6
parent 3751 7f33a2015381
child 3753 5fd734bed0d4
Updated usage information for tool "usedir".
doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Tue Sep 30 17:28:54 1997 +0200
+++ b/doc-src/System/misc.tex	Tue Sep 30 17:29:32 1997 +0200
@@ -140,14 +140,13 @@
 
 The \tooldx{usedir} utility builds object-logic images, or runs
 example sessions based on existing logics. Its usage is:
-%FIXME
-%    -g BOOL      generate theory graph data (default false)
 \begin{ttbox}
-Usage: isatool usedir LOGIC NAME
+Usage: usedir LOGIC NAME
 
   Options are:
     -b           build mode (output heap image, use dir ".")
-    -h BOOL      generate theory HTML data (default false)
+    -i BOOL      generate theory browsing information,
+                 i.e. HTML / graph data (default false)
     -s NAME      override session NAME
 
   Build object-logic or run examples. Also creates browsing
@@ -182,9 +181,9 @@
 \texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML}
 commands to run the desired examples.
 
-\medskip The \texttt{-h} option controls HTML browsing data
+\medskip The \texttt{-i} option controls theory browsing data
 generation. It may be explicitely turned on or off --- the last
-occurrence of some \texttt{-h} on the command line wins.
+occurrence of some \texttt{-i} on the command line wins.
 
 \medskip Any \texttt{usedir} session is named by some \emph{session
   identifier}. These accumulate, documenting the way sessions depend