diff tests/coverage.py @ 2424:092039246d73

Report on push/pull if heads are merged, too, like for new heads. Use case: If a remote repo has two heads and I _want_ to merge them, I merge and push. Meanwhile someone else pushed on top of one of the heads. He won't get a warning, because he doesn't create a new head, I won't notice that I don't close a head, because I don't get a message telling me.
author Thomas Arendsen Hein <thomas@intevation.de>
date Sat, 10 Jun 2006 17:39:29 +0200
parents d3bddedfdbd0
children 53e843840349
line wrap: on
line diff