Hi all,

I screwed up some commits in the near past so now I have used the git weapon of mass destruction a.k.a. GFB. The history is changed, so, please, do not pull to your repositories! Use a fresh clone, or fetch, instead.

Sorry for the inconvenience. r.