[isabelle-dev] NEWS

Makarius makarius at sketis.net
Tue Dec 2 22:03:59 CET 2008

On Wed, 3 Dec 2008, Gerwin Klein wrote:

> Makarius wrote:
> > Of course, heaps produced inside the repository file space like that must
> > not be committed.
> We might want to add an .hgignore file and put ^heaps/ in it. This should at
> least make accidental commits less likely.

It is already there, together with some other things that people tend to 
commit by accident:

syntax: glob


syntax: regexp


In fact, accidental commits are not yet a desaster, because they are local 
only and can be repaired.  Only an actual push will make things last 


More information about the isabelle-dev mailing list