mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Wed, 10 Dec 2003, David Allouche wrote:
> On Wed, Dec 10, 2003 at 11:02:48AM +0100, Joris van der Hoeven wrote:
> > On Wed, 10 Dec 2003, Valery Pipin wrote:
> > > Is it possible to change the time option for  autosaving the document or
> > > session?
> >
> > No, there is not, but it should not be extremely difficult to hack
> > the sources to create such an option (even though several files would
> > need to be changed). I have no time for this right now.
>
> Done. Patch attached to this message.

Thanks; the patch has been applied for the next version.

> Not what I would call an "easy" patch though.

No, but just creating a patch with an option to disable autosaving
would not have been very difficult either. Anyway, being able to
select the autosave time is even better.