On 11/06/2012 07:54 PM, Gerwin Klein wrote:
The approach in LaTeX Sugar is very similar, but I don't remember if we
describe there how to avoid generating the superfluous pdf.
You can basically use a script document/build that takes over control of which commands
are run to build the document. That command could for instance just be "touch
document.pdf" if you don't want to build anything at all in that run.
Right! I actually tried before that and was only too stupid to make it
work, since I wrote
touch snipped.pdf
where it should have been
touch ../snipped.pdf
Thanks for reminding me. With the correct path it works.
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
