Closed pmai closed 7 months ago
Can be closed as part of #758 ?
Can be closed as part of #758 ?
No, this is a separate matter, #758 just depends on this PR, hence it is already based on the same branch to avoid later merge conflicts. Since this one has already been reviewed, we'll discuss separately.
OK, this is good to be merged!
CCB 2024-01-15: Merge as-is.
Reviewed for v3.7.0
fixes #741