I already fixed that, but likely I made an error in "git rebase -i" before
pushing to master.
Signed-off-by: Alessandro Rubini <rubini@gnudd.com>