[isabelle-dev] NEWS

[Gerwin Klein]

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.

Gerwin