diff options
author | Mike Frysinger <vapier@google.com> | 2020-01-25 03:07:27 -0500 |
---|---|---|
committer | Treehugger Robot <treehugger-gerrit@google.com> | 2020-01-27 05:01:36 +0000 |
commit | 3636ca90dd5169f4310ad8bdb2641a67f58265d6 (patch) | |
tree | 2d7c8b1a93c331227d511cb06a086317cc75fcbb /.github | |
parent | 47654174e1e9e4ca5c90ae62f95b74013014a9bf (diff) | |
download | minijail-3636ca90dd5169f4310ad8bdb2641a67f58265d6.tar.gz |
github: support mistaken-pull-closer for automatically clearing incoming PRs
Change-Id: I32598a944006cc5e37fb6db64eb937cb0721d18f
Diffstat (limited to '.github')
-rw-r--r-- | .github/mistaken-pull-closer.yml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/.github/mistaken-pull-closer.yml b/.github/mistaken-pull-closer.yml new file mode 100644 index 0000000..eb4cb89 --- /dev/null +++ b/.github/mistaken-pull-closer.yml @@ -0,0 +1,17 @@ +# The JSONPath filter expression used to identify which PRs to close. +# The data filtered is the pull request data along with other metadata passed in +# by probot. +# See https://goessner.net/articles/JsonPath/ +# `true` will close all PRs. +filters: + - true + +# The message to post to the closed PR. +commentBody: | + Thanks for your contribution! Unfortunately, we don't use GitHub pull + requests to manage code contributions to this repository. Instead, please + see [README.md](../blob/master/README.md) which provides full instructions + on how to get involved. + +# Whether to add a label to the closed PR. +addLabel: false |