merge bugfix X-(

Looks to have first been introduced in Sep 2023. (Merge commit 09c76c82c2, though git's merge commits are hard to read. Yes, looks like commit 0a12e4c733 (Pijul change NVSC4N4KMUHGX5FEOM2DXYA4VHEEQTP3QNY3D7WY4UONVW5LCT2QC) didn't get merged right.)

Created by  akkartik  on June 21, 2024
OEISQSEARCRFERL4XGGIN2KPLUBKB2IZOBEXY7ETFGR77YHIISLAC
Change contents