6da5d9f4e5
We need the same source tree for 32-bit as for 64-bit builds for
files/patch-man not to break things.
Also revert f48100735d which was harmless, alas not helpful.
PR: 204227