diff -r f57de4a9eb9c -r f037aa6699c3 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 09:27:47 2010 -0800 +++ b/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 21:26:21 2010 +0100 @@ -198,14 +198,19 @@ Usage: browser [OPTIONS] [GRAPHFILE] Options are: + -b Admin/build only -c cleanup -- remove GRAPHFILE after use -o FILE output to FILE (ps, eps, pdf) \end{ttbox} When no filename is specified, the browser automatically changes to the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}. - \medskip The \verb|-c| option causes the input file to be - removed after use. + \medskip The \verb|-b| option indicates that this is for + administrative build only, i.e.\ no browser popup if no files are + given. + + The \verb|-c| option causes the input file to be removed + after use. The \verb|-o| option indicates batch-mode operation, with the output written to the indicated file; note that \verb|pdf|