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:
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