Filtering of git repository

Unless somebody protests, the plan is now as follows:

On Sunday (the 12:th), sometime between 10:00 and 18:00 UTC, I will replace pike.git with a filtered version. The original pike.git will become available under the name pike-old.git. Complete mappings between the commit sha:s of the two repositories will also be published, to aid manual rebasing and similar housekeeping.

I would appreciate if no new commits were pushed to the repository during this time, unless I have announced that the activity has been either completed or cancelled.

As for the cherry-pick conversion, no notes or extra annotations to the commit messages will be added. Instead, I will log the relevant sha:s to facilitate adding notes at a later time.