On 2016-06-13 10:33, Walter Bright wrote:

No, have to do that manually.

I'm pretty sure I've seen something that looks automated. Could that be for when a PR is merged?

--
/Jacob Carlborg

Reply via email to