# HG changeset patch
# User wenzelm
# Date 962665853 -7200
# Node ID 161fb7f00414b74d53d2b0b2e59e14f314d2329a
# Parent  899b83e8d2e186c999818c8019e0cdea40d2b8fd
fixed usage;

diff -r 899b83e8d2e1 -r 161fb7f00414 doc-src/System/present.tex
--- a/doc-src/System/present.tex	Tue Jul 04 01:10:36 2000 +0200
+++ b/doc-src/System/present.tex	Tue Jul 04 01:10:53 2000 +0200
@@ -124,7 +124,10 @@
 The stand-alone version of the graph browser is wrapped up as an
 Isabelle tool called \tooldx{browser}:
 \begin{ttbox}
-Usage: browser [GRAPHFILE]
+Usage: browser [OPTIONS] [GRAPHFILE]
+
+  Options are:
+    -d           delete file after use
 \end{ttbox}
 When no filename is specified, the browser automatically changes to the
 directory \texttt{ISABELLE_BROWSER_INFO}.
@@ -360,7 +363,7 @@
 including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}
 and an optional \texttt{document} directory.  Its usage is:
 \begin{ttbox}
-Usage: mkdir [LOGIC] NAME
+Usage: mkdir [OPTIONS] [LOGIC] NAME
 
   Options are:
     -I FILE      alternative IsaMakefile output
@@ -428,7 +431,7 @@
 The \tooldx{usedir} utility builds object-logic images, or runs example
 sessions based on existing logics. Its usage is:
 \begin{ttbox}
-Usage: usedir LOGIC NAME
+Usage: usedir [OPTIONS] LOGIC NAME
 
   Options are:
     -D PATH      dump generated document sources into PATH
diff -r 899b83e8d2e1 -r 161fb7f00414 lib/Tools/browser
--- a/lib/Tools/browser	Tue Jul 04 01:10:36 2000 +0200
+++ b/lib/Tools/browser	Tue Jul 04 01:10:53 2000 +0200
@@ -10,7 +10,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [GRAPHFILE]"
+  echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
   echo
   echo "  Options are:"
   echo "    -d           delete file after use"
diff -r 899b83e8d2e1 -r 161fb7f00414 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Tue Jul 04 01:10:36 2000 +0200
+++ b/lib/Tools/mkdir	Tue Jul 04 01:10:53 2000 +0200
@@ -12,7 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [LOGIC] NAME"
+  echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
   echo
   echo "  Options are:"
   echo "    -I FILE      alternative IsaMakefile output"
diff -r 899b83e8d2e1 -r 161fb7f00414 lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Jul 04 01:10:36 2000 +0200
+++ b/lib/Tools/usedir	Tue Jul 04 01:10:53 2000 +0200
@@ -12,7 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG LOGIC NAME"
+  echo "Usage: $PRG [OPTIONS] LOGIC NAME"
   echo
   echo "  Options are:"
   echo "    -D PATH      dump generated document sources into PATH"