doc-src/System/Thy/document/Sessions.tex
changeset 48805 c3ea910b3581
parent 48739 3a6c03b15916
child 48814 d488a5f25bf6
     1.1 --- a/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 13:40:49 2012 +0200
     1.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 15:42:58 2012 +0200
     1.3 @@ -471,19 +471,16 @@
     1.4  \isamarkuptrue%
     1.5  %
     1.6  \begin{isamarkuptext}%
     1.7 -The following produces an example session as separate
     1.8 -  directory called \verb|Test|:
     1.9 +Produce session \verb|Test| within a separate directory
    1.10 +  of the same name:
    1.11  \begin{ttbox}
    1.12 -isabelle mkroot Test && isabelle build -v -D Test
    1.13 +isabelle mkroot Test && isabelle build -D Test
    1.14  \end{ttbox}
    1.15  
    1.16 -  Option \verb|-v| is not required, but useful to reveal the
    1.17 -  the location of generated documents.
    1.18 -
    1.19 -  \medskip The subsequent example turns the current directory to a
    1.20 -  session directory with document and builds it:
    1.21 +  \medskip Upgrade the current directory into a session ROOT with
    1.22 +  document preparation, and build it:
    1.23  \begin{ttbox}
    1.24 -isabelle mkroot -d && isabelle build -D.
    1.25 +isabelle mkroot -d && isabelle build -D .
    1.26  \end{ttbox}%
    1.27  \end{isamarkuptext}%
    1.28  \isamarkuptrue%