Subject: Re: [PATCH 5/8] doc: remove redundant rm

From: Ævar Arnfjörð Bjarmason <[email-masked]>
Date: Thu, 13 May 2021 17:22:37 +0200

On Wed, May 12 2021, Felipe Contreras wrote:

> It's not clear what it was supposed to achieve.

It seems this used to make sense around 7b8a74f39cb (Documentation:
Replace @@GIT_VERSION@@ in documentation, 2007-03-25), but at some point
(I didn't look further) we refactored that and kept the "rm".