Dummy commit to try if we can close some old github PRs via commit-comments: closes #2, closes #3, closes #4, closes #19