On Sun, Aug 19, 2018 at 05:52:06PM +0200, Julien Lepiller wrote:
> Pushed as dd1e45335e135fe724acece440782344ef8ca9fd in staging with
> your suggestions. And now I wonder why I pushed to staging since it
> doesn't change any existing package... too late I guess :)

If you use `git cherry-pick` to apply the commit to the master branch,
Git should do the right thing when staging is eventually merged to
master.