Subject: Re: bug#13107: timestamp bug when files are created just before make is run

From: Karl Berry <[email-masked]>
Date: Sat, 11 Jul 2020 19:23:45 -0600

Given the zero response, it seems undesirable to add even minor
complexity to support something which may no longer be needed.
Closing. -k