Thanks, the pull request was merged manually:

• changes to git ignore made its own commit
• patch to db_postgres had the commit message re-using the pull request title, because that is the right format for the commit message

—
Reply to this email directly or view it on GitHub.