# HG changeset patch # User wenzelm # Date 1513013964 -3600 # Node ID d5e51ba2156159204621b876be84f29f36625fad # Parent ecc786cb3b7bc0fbdd1a6c3176b52634471d91d9 updated documentation; diff -r ecc786cb3b7b -r d5e51ba21561 src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Mon Dec 11 17:52:05 2017 +0100 +++ b/src/Doc/System/Presentation.thy Mon Dec 11 18:39:24 2017 +0100 @@ -151,7 +151,6 @@ \Usage: isabelle document [OPTIONS] Options are: - -c aggressive cleanup of -d DIR content -d DIR document output directory (default "output/document") -n NAME document name (default "document") -o FORMAT document format: pdf (default), dvi @@ -168,12 +167,6 @@ run. \<^medskip> - The \<^verbatim>\-c\ option tells @{tool document} to dispose the document sources - after successful operation! This is the right thing to do for sources - generated by an Isabelle process, but take care of your files in manual - document preparation! - - \<^medskip> Option \<^verbatim>\-d\ specifies an laternative document output directory. The default is \<^verbatim>\output/document\ (derived from the document name). Note that the result will appear in the parent of this directory. @@ -240,10 +233,10 @@ we recommend to include \<^file>\~~/lib/texinputs/pdfsetup.sty\ as well. \<^medskip> - As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\-c\ is - run on the resulting copy of the \<^verbatim>\document\ directory. Thus the actual - output document is built and installed in its proper place. The generated - sources are deleted after successful run of {\LaTeX} and friends. + As a final step of Isabelle document preparation, @{tool document} is run on + the generated \<^verbatim>\output/document\ directory. Thus the actual output document + is built and installed in its proper place. The generated sources are + deleted after successful run of {\LaTeX} and friends. Some care is needed if the document output location is configured differently, say within a directory whose content is still required