I think this is OK, but a bit borderline. I'm accepting as is, but have posted "for the record" to recheck later. If we have to make further changes, we'll do so in a different PR>

[mjang]

          I think this is OK, but a bit borderline. I'm accepting as is, but have posted "for the record" to recheck later. If we have to make further changes, we'll do so in a different PR>

Originally posted by @mjang in #511 (comment)

[github-actions]

This issue is stale because it has been open for 90 days with no activity. Remove the stale label or add a comment to keep it open. If you do not take action, this will be closed in 10 days.

[github-actions]

This issue was closed after 100 days of inactivity.