Oops, the shown patch in the last mail was incomplete. See http://git.sv.gnu.org/gitweb/?p=gnulib.git;a=commitdiff;h=b442459322dbef0bcb547770565b05724e98b47d for the full patch.
(Sorry, a 'git' pitfall. I had used 'git add' on one file and not on the other. What is the command to get the union of "git diff" and "git diff --cached"?) Bruno
