# 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 @@
 \<open>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>\<open>-c\<close> 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>\<open>-d\<close> specifies an laternative document output directory. The default
   is \<^verbatim>\<open>output/document\<close> (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>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
 
   \<^medskip>
-  As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
-  run on the resulting copy of the \<^verbatim>\<open>document\<close> 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>\<open>output/document\<close> 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