Subject: Re: bug#13107: timestamp bug when files are created just before make is run
From: Karl Berry <[email-masked]>
To: [email-masked]
Date: Sat, 11 Jul 2020 19:23:45 -0600
List-Id: <debbugs-submit.debbugs.gnu.org>

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