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.