[isabelle-dev] NEWS: session 'document_files'
Tobias Nipkow
nipkow at in.tum.de
Sun Apr 13 12:23:03 CEST 2014
That works fine, thank you.
Tobias
On 11/04/2014 23:52, Makarius wrote:
> On Fri, 11 Apr 2014, Tobias Nipkow wrote:
>
>> What I sometimes need is to have the latex files generated but not processed.
>> Currently I achieve this with a dummy root.tex file that includes nothing. Is
>> there a less dummy way?
>
> There is no need for root.tex and latex to produce a dummy root.pdf. This can be
> done more directly via some document/build script that merely does "touch
> root.pdf". See the included example session.
>
> That is functionality from the summer 2012 reform, and I am rather glad that the
> number of build options was successfully reduced, while it has become more general.
>
> If there is a strong need for it, one could add some option to the "isabelle
> mkroot" tool to produce such a setup -- it presently uses only 2 letters of the
> alphabet for options.
>
>
> Makarius
More information about the isabelle-dev
mailing list