Backport of docs: document behaviour of tls.https.verify_outgoing into release/1.14.x #5889
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # The outline of this workflow is something that the GitHub Security team warns against | |
| # here: https://securitylab.github.com/research/github-actions-preventing-pwn-requests. But | |
| # due to this workflow only running a git diff check and not building or publishing anything, | |
| # there is no harm in checking out the PR HEAD code. | |
| # | |
| # All the code checked out in this workflow should be considered untrusted. This workflow must | |
| # never call any makefiles or scripts. It must never be changed to run any code from the checkout. | |
| # This workflow posts a message to a PR to remind maintainers that there are website/ changes | |
| # in the PR and if they need to be cherry-picked to the stable-website branch, the | |
| # 'type/docs-cherrypick' label needs to be applied. | |
| name: Website Checker | |
| on: | |
| pull_request_target: | |
| types: [opened] | |
| # Runs on PRs to main and all release branches | |
| branches: | |
| - main | |
| - release/* | |
| jobs: | |
| # checks that a 'type/docs-cherrypick' label is attached to PRs with website/ changes | |
| website-check: | |
| # If there's already a `type/docs-cherrypick` label or an explicit `pr/no-docs` label, we ignore this check | |
| if: >- | |
| !contains(github.event.pull_request.labels.*.name, 'type/docs-cherrypick') && | |
| !contains(github.event.pull_request.labels.*.name, 'pr/no-docs') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| fetch-depth: 0 # by default the checkout action doesn't checkout all branches | |
| - name: Check for website/ dir change in diff | |
| run: | | |
| # check if there is a diff in the website/ directory | |
| website_files=$(git --no-pager diff --name-only HEAD "$(git merge-base HEAD "origin/${{ github.event.pull_request.base.ref }}")" -- website/) | |
| # If we find changed files in the website/ directory, we post a comment to the PR | |
| if [ -n "$website_files" ]; then | |
| # post PR comment to GitHub to check if a 'type/docs-cherrypick' label needs to be applied to the PR | |
| echo "website-check: Did not find a 'type/docs-cherrypick' label, posting a reminder in the PR" | |
| github_message="🤔 This PR has changes in the \`website/\` directory but does not have a \`type/docs-cherrypick\` label. If the changes are for the next version, this can be ignored. If they are updates to current docs, attach the label to auto cherrypick to the \`stable-website\` branch after merging." | |
| curl -s -H "Authorization: token ${{ secrets.PR_COMMENT_TOKEN }}" \ | |
| -X POST \ | |
| -d "{ \"body\": \"${github_message}\"}" \ | |
| "https://api.github.com/repos/${GITHUB_REPOSITORY}/issues/${{ github.event.pull_request.number }}/comments" | |
| fi |