Subject: close 49381

From: Paul Eggert <[email-masked]>
Date: Thu, 10 Feb 2022 11:09:29 -0800

close 49381
thanks
Intended to close it in July, but forgot to actually close it.