I don't see anyting wrong with the patch, but... +bug reports may be [...] posted to the Usenet newsgroup > .BR gnu.bash.bug . >
Ummm? Does Chet still read Usenet? Does anyone else? -Martin PS: Sometimes I miss the good old days when Usenet was the social glue that held a small worldwide community or techies together, before we gave away our autonomy and agency to centralized services. And before Eternal September, when the hoards broke everything; 11408 days and counting. PPS: as far as I know, Google was the last large provider giving access to Usenet, and they shut down their inward feed about 5 months ago. A search finds a few people on Reddit still using it, presumably by direct peering, but they only seem interested in using it as a way to exchange files - with the subtext that it's to circumvent copyright protections.