RFR: 60: Add `integrated` to closed pull requests that have been integrated

[Erik Duveblad via github.com]

On Mon, 19 Aug 2019 12:27:27 GMT, Robin Westberg via github.com <duke at openjdk.java.net> wrote:

> Hi all,
> 
> Please review this change that adds an 'integrated' label to a PR after it has been integrated.
> 
> Best regards,
> Robin
> 
> ----------------
> 
> Commits:
>  - 85af475c:	Add integrated label to PRs when integrating them
> 
> Pull request:
> https://git.openjdk.java.net/skara/pull/58
> 
> Webrev:
> https://webrevs.openjdk.java.net/skara/58/webrev.00
> 
> Patch:
> https://git.openjdk.java.net/skara/pull/58.diff
> 
> Fetch command:
> git fetch https://git.openjdk.java.net/skara pull/58/head:pull/58

This PR has been reviewed by Erik Duveblad via github.com - changes are approved. Review comment:

Looks good, nice feature!

PR: https://git.openjdk.java.net/skara/pull/58