merge maint into master

[Akim Demaille]

I love git.  Since tabulations were removed in master
but not in maint, -s recursive -X ignore-all-space saves
the day.

merge.patch
Description: Binary data