sorry to do this twice - just noticed the page was a bit mixed up
merged
mentioned in commit c63e4de6
You can go ahead and push right to the repo -- no need for merge requests. Looks like you're a master of this project, so you should be able to...
