Subject: Re: bug#76123: [PATCH] Eliminate savehist duplicated symbols
From: Eli Zaretskii <[email-masked]>
To: Ship Mints <[email-masked]>
Cc: [email-masked], [email-masked]
Date: Sat, 08 Feb 2025 14:07:58 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

> From: Ship Mints <[email-masked]>
> Date: Sat, 8 Feb 2025 05:38:47 -0500
> Cc: [email-masked], [email-masked]
> 
> Surely. Revised patch attached with a NEWS entry.

Thanks, installed on master, and closing the bug.

> I did not yet combine the two tests (the code is nearly duplicated) if that's what you think should be done so
> if you want me to do that, I can today.

I see no need.