Re: git is live

Tom Tromey
2013-11-08T19:40:57Z

Tom> The two messages refer to two different commits.

Andreas> It would be easier to notice if they would mention the branch.

Good idea. I checked in a patch that should fix this.

Tom