Merged repo for protocol headers? Why are they split?

[Daniel Martin]

On 6 December 2017 at 16:23, Gioele Barabucci <gioele at svario.it> wrote:
> Hi,
>
> 06.12.2017 13:37 Daniel Martin:
>>
>> PS: Just talked to Peter, he's okay with filter-branch as it gives us
>> git-log without a struggle and references to other commits can be
>> looked up in the old repos
>
> A suggestion: you could add the old IDs into the new commit logs. This makes
> it possible to search for old commits with a simple grep.
>
> You can do this with a `--msg-filter` pass like the following one. This
> filter must be run before `filter_branch_prefix_subject`.
>
>     git filter-branch --msg-filter '
>         cat && echo && echo "Original-Commit-ID: $GIT_COMMIT"
>     ' $branch

Thanks for the tip. Added.