dolfin team mailing list archive

[Johan Jansson <jjan@xxxxxxxxxxx>]

On Tue, Jan 09, 2007 at 04:00:32PM +0100, Anders Logg wrote:
> We have more than one head in the repository (check with hg heads).
> Is it ok if I remove all other heads than tip? I guess no one is using
> any of them.
> 
> /Anders

I'm fine with removing all the other heads, they aren't used.

  Johan