src/Doc/System/Presentation.thy
changeset 67351 63d7aca15f6b
parent 67263 449a989f42cd
child 67399 eab6ce8368fa
equal deleted inserted replaced
67350:f061129d891b 67351:63d7aca15f6b
   165   options. It may be manually invoked on the generated browser information
   165   options. It may be manually invoked on the generated browser information
   166   document output as well, e.g.\ in case of errors encountered in the batch
   166   document output as well, e.g.\ in case of errors encountered in the batch
   167   run.
   167   run.
   168 
   168 
   169   \<^medskip>
   169   \<^medskip>
   170   Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
   170   Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
   171   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   171   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   172   will appear in the parent of this directory.
   172   will appear in the parent of this directory.
   173 
   173 
   174   \<^medskip>
   174   \<^medskip>
   175   The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
   175   The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,