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".
