mirror of
https://github.com/google/re2.git
synced 2026-10-28 08:24:42 +08:00
.github/workflows: delete pr.yml
Allow pull requests. Going to try not using Gerrit.
This commit is contained in:
2 files changed
-35
No files matched your search
@@ -1,34 +0,0 @@
|
||||
name: PR
|
||||
on:
|
||||
pull_request_target:
|
||||
branches: [main]
|
||||
types: [opened]
|
||||
permissions:
|
||||
contents: read
|
||||
jobs:
|
||||
close:
|
||||
permissions:
|
||||
contents: read
|
||||
# We have to use two different APIs below,
|
||||
# so just grant two different permissions.
|
||||
issues: write
|
||||
pull-requests: write
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v4.2.2
|
||||
- uses: actions/github-script@v7.0.1
|
||||
with:
|
||||
script: |
|
||||
const fs = require('fs');
|
||||
console.log(await github.rest.issues.createComment({
|
||||
owner: context.repo.owner,
|
||||
repo: context.repo.repo,
|
||||
issue_number: context.issue.number,
|
||||
body: fs.readFileSync('CONTRIBUTING.md', { encoding: 'utf8', }),
|
||||
}));
|
||||
console.log(await github.rest.pulls.update({
|
||||
owner: context.repo.owner,
|
||||
repo: context.repo.repo,
|
||||
pull_number: context.issue.number,
|
||||
state: 'closed',
|
||||
}));
|
||||
@@ -1,2 +1 @@
|
||||
RE2 uses Gerrit instead of GitHub pull requests.
|
||||
See the [Contribute](https://github.com/google/re2/wiki/Contribute) wiki page.
|
||||
Reference in new issue
Block a user