Patch pushed as d1072f21ba446fe470b171575f5e3202aef17a04 with shorter
names for the patches, and I also added them to the 'dist_patch_DATA'
list of patches in "gnu/local.mk".
Thanks.