fixed usage;
authorwenzelm
Tue Jul 04 01:10:53 2000 +0200 (2000-07-04)
changeset 9237161fb7f00414
parent 9236 899b83e8d2e1
child 9238 ad37b21c0dc6
fixed usage;
doc-src/System/present.tex
lib/Tools/browser
lib/Tools/mkdir
lib/Tools/usedir
     1.1 --- a/doc-src/System/present.tex	Tue Jul 04 01:10:36 2000 +0200
     1.2 +++ b/doc-src/System/present.tex	Tue Jul 04 01:10:53 2000 +0200
     1.3 @@ -124,7 +124,10 @@
     1.4  The stand-alone version of the graph browser is wrapped up as an
     1.5  Isabelle tool called \tooldx{browser}:
     1.6  \begin{ttbox}
     1.7 -Usage: browser [GRAPHFILE]
     1.8 +Usage: browser [OPTIONS] [GRAPHFILE]
     1.9 +
    1.10 +  Options are:
    1.11 +    -d           delete file after use
    1.12  \end{ttbox}
    1.13  When no filename is specified, the browser automatically changes to the
    1.14  directory \texttt{ISABELLE_BROWSER_INFO}.
    1.15 @@ -360,7 +363,7 @@
    1.16  including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}
    1.17  and an optional \texttt{document} directory.  Its usage is:
    1.18  \begin{ttbox}
    1.19 -Usage: mkdir [LOGIC] NAME
    1.20 +Usage: mkdir [OPTIONS] [LOGIC] NAME
    1.21  
    1.22    Options are:
    1.23      -I FILE      alternative IsaMakefile output
    1.24 @@ -428,7 +431,7 @@
    1.25  The \tooldx{usedir} utility builds object-logic images, or runs example
    1.26  sessions based on existing logics. Its usage is:
    1.27  \begin{ttbox}
    1.28 -Usage: usedir LOGIC NAME
    1.29 +Usage: usedir [OPTIONS] LOGIC NAME
    1.30  
    1.31    Options are:
    1.32      -D PATH      dump generated document sources into PATH
     2.1 --- a/lib/Tools/browser	Tue Jul 04 01:10:36 2000 +0200
     2.2 +++ b/lib/Tools/browser	Tue Jul 04 01:10:53 2000 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  function usage()
     2.5  {
     2.6    echo
     2.7 -  echo "Usage: $PRG [GRAPHFILE]"
     2.8 +  echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
     2.9    echo
    2.10    echo "  Options are:"
    2.11    echo "    -d           delete file after use"
     3.1 --- a/lib/Tools/mkdir	Tue Jul 04 01:10:36 2000 +0200
     3.2 +++ b/lib/Tools/mkdir	Tue Jul 04 01:10:53 2000 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  function usage()
     3.5  {
     3.6    echo
     3.7 -  echo "Usage: $PRG [LOGIC] NAME"
     3.8 +  echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
     3.9    echo
    3.10    echo "  Options are:"
    3.11    echo "    -I FILE      alternative IsaMakefile output"
     4.1 --- a/lib/Tools/usedir	Tue Jul 04 01:10:36 2000 +0200
     4.2 +++ b/lib/Tools/usedir	Tue Jul 04 01:10:53 2000 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  function usage()
     4.5  {
     4.6    echo
     4.7 -  echo "Usage: $PRG LOGIC NAME"
     4.8 +  echo "Usage: $PRG [OPTIONS] LOGIC NAME"
     4.9    echo
    4.10    echo "  Options are:"
    4.11    echo "    -D PATH      dump generated document sources into PATH"