so, the string-in-commit (e.g. ‘Fixes #1234’) in an RB comment seems to make github auto-close the PR and even references the commit that closed it.