Integrated: 1853: Make it possible to disable merge PRs for a repository

[Zhao Song]

On Mon, 10 Apr 2023 20:16:54 GMT, Zhao Song <zsong at openjdk.org> wrote:

> In this patch, PR bot has been added with the capability to control whether merge-style pr is allowed in specific repositories.
> 
> By default, merge-style pr is enabled.
> 
> However, if it is desired to disable merge-style pr in a repo, the configuration can be added to the PR bot configuration as follows:
> 
> {
>   "pr": {
>       "repositories": {
>           "repo1": {
>                "merge": false
>           }
>        }
>   }
> }
> 
> 
> If merge-style pr is disabled and the title of the pr matches the pattern of merge-style pr, the pr bot would reply a warning message to the user and prompt for the next steps.

This pull request has now been integrated.

Changeset: 0b01ba53
Author:    Zhao Song <zsong at openjdk.org>
URL:       https://git.openjdk.org/skara/commit/0b01ba53e694c261ebbaca20142bf96cd7757f22
Stats:     87 lines in 6 files changed: 85 ins; 0 del; 2 mod

1853: Make it possible to disable merge PRs for a repository

Reviewed-by: erikj

-------------

PR: https://git.openjdk.org/skara/pull/1499