Re: [isabelle] LaTeX document



On Friday 22 September 2006 11:32, Francisco Jose CHAVES ALONSO wrote:
> > I need the TeX file generated by Isabelle, to extract some parts
> > for another document that I also generate with another command.
> > "isatool make" delete the TeX generated file. It is possible to
> > save it?

On Saturday 23 September 2006 17:10, Martin Ellis wrote:
> I have a patch for Pure which does a few things, including this.

Uh... on second thoughts, if you're not already poking about with 
Pure, it's going to be much easier to edit lib/Tools/document - this 
looks like it might be the offending line:

   [ -n "$CLEAN" ] && rm -rf "$DIR"

Martin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.