src/Doc/System/Presentation.thy
changeset 67069 f11486d31586
parent 67043 848672fcaee5
child 67139 8fe0aba577af
     1.1 --- a/src/Doc/System/Presentation.thy	Mon Nov 13 15:00:21 2017 +0100
     1.2 +++ b/src/Doc/System/Presentation.thy	Mon Nov 13 15:07:03 2017 +0100
     1.3 @@ -98,6 +98,7 @@
     1.4  
     1.5    Options are:
     1.6      -A LATEX     provide author in LaTeX notation (default: user name)
     1.7 +    -I           init Mercurial repository and add generated files
     1.8      -T LATEX     provide title in LaTeX notation (default: session name)
     1.9      -n NAME      alternative session name (default: directory base name)
    1.10  
    1.11 @@ -116,6 +117,9 @@
    1.12    Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
    1.13    using {\LaTeX} source notation.
    1.14  
    1.15 +  Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
    1.16 +  adds all generated files (without commit).
    1.17 +
    1.18    Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
    1.19    of the given directory is used.
    1.20