[isabelle-dev] NEWS

[Makarius]

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

*~
*.class
*.jar
.DS_Store


syntax: regexp

^heaps/
^browser_info/
...

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 
forever.


	Makarius