| FazBrowse GitHub Viewer | Trending | | Home |
| Tools: [Download Repo ZIP] [Original HTTPS Page] |
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| name: PR dequeued | ||
|
|
||
| on: | ||
| pull_request: | ||
| types: | ||
| - dequeued | ||
|
|
||
| jobs: | ||
| notify: | ||
|
Comment thread
mbg marked this conversation as resolved.
Resolved
|
||
| name: Notify | ||
| runs-on: ubuntu-slim | ||
|
|
||
| if: github.event.pull_request.merged != true | ||
|
|
||
| permissions: | ||
| pull-requests: write | ||
|
|
||
| steps: | ||
| - name: Notify that the PR was removed from the merge queue | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | ||
| PR_NUMBER: ${{ github.event.pull_request.number }} | ||
| REASON: ${{ github.event.reason }} | ||
| USER: ${{ github.event.pull_request.user.login }} | ||
| run: | | ||
| echo "@$USER The pull request was removed from the merge queue (\`$REASON\`)." \ | ||
| "Please resolve any issues if required and enqueue the PR again." | | ||
| gh pr comment --body-file - --repo github/codeql-action "$PR_NUMBER" | ||
| Back | FazBrowse Home | New Git URL |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Choose a reason Spam Abuse Off Topic Outdated Duplicate Resolved Low QualityAbsolutely not.
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.