git repo mirroring

["Simon 'corecode' Schubert" <corecode@xxxxxxxxxxxx>]

Hey,

this is just a note to all people mirroring the git repo, and those who 
want to tidy their source repos:

Recently we had a small accident which led to another branch being created 
in our repo.  No big deal, that's very cheap.  Now that I cleaned the 
branch from the repo it turned out that chlamydia wasn't syncing this 
removal of the branch.

This is because I was only running "git remote update".  This however is 
not sufficient to track all changes (i.e. branch removals) from the 
remote.  You will have to augment your sync scripts to run

	git remote prune $(git remote)

in addition to

	git remote update

Please update your sync scripts, because I am sure this won't be the last 
time that we want to delete a head from the repo.

cheers
  simon

--
  <3 the future  +++  RENT this banner advert  +++   ASCII Ribbon   /"\
  rock the past  +++  space for low €€€ NOW!1  +++     Campaign     \ /
Party Enjoy Relax   |   http://dragonflybsd.org      Against  HTML   \
Dude 2c 2 the max   !   http://golden-apple.biz       Mail + News   / \