Subject: Re: bug#61078: [PATCH 0/4] Rename '/fixed' by '/pinned'

From: Ludovic Courtès <[email-masked]>
Date: Tue, 31 Jan 2023 23:46:53 +0100

Hi Simon,

Overall the 4 patches LGTM, thanks for doing this!

One thing came to mind though:

Simon Tournier <[email-masked]> skribis:

> -(define-public git-minimal/fixed
> +(define-public git-minimal/pinned

Should we also add:

  (define-deprecated/public-alias git-minimal/fixed git-minimal/pinned)

and similarly for the other patches?

Seems like it would be safer and we can remove it later (a couple of
months may be enough).

Ludo’.