add 3d-print docs #20
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
| ################################################################################ | |
| # File: .github/workflows/unicode_warn.yml | |
| # Version: 0.6 | |
| # Purpose: Detects Unicode in PRs and comments the results of findings in PR | |
| # Authors: Michael Altfield <michael@michaelaltfield.net> | |
| # Created: 2021-11-20 | |
| # Updated: 2024-08-08 | |
| ################################################################################ | |
| # in main branch | |
| name: malicious_sanity_checks | |
| # execute this workflow automatically on all PRs | |
| on: | |
| pull_request_target: | |
| types: [opened, edited, synchronize, reopened, unlocked] | |
| jobs: | |
| unicode_warn: | |
| runs-on: ubuntu-latest | |
| container: debian:bullseye-slim | |
| permissions: | |
| issues: write | |
| pull-requests: write | |
| steps: | |
| - name: Dump GitHub context | |
| env: | |
| GITHUB_CONTEXT: ${{ toJSON(github) }} | |
| run: echo "$GITHUB_CONTEXT" | |
| - name: Prereqs | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| apt-get update | |
| apt-get install -y git bsdmainutils curl jq | |
| git clone "https://token:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" . | |
| shell: bash | |
| - name: Get link to this run | |
| run: | | |
| # https://stackoverflow.com/a/75734917 | |
| workflow_id=$(curl -L \ | |
| -H "Accept: application/vnd.github+json" \ | |
| -H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}"\ | |
| -H "X-GitHub-Api-Version: 2022-11-28" \ | |
| https://api.github.com/repos/${GITHUB_REPOSITORY}/actions/runs/${GITHUB_RUN_ID}/attempts/${GITHUB_RUN_ATTEMPT}/jobs | jq .jobs[].id ) | |
| RUN_URL=https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}/job/${workflow_id} | |
| echo "RUN_URL=${RUN_URL}" >> $GITHUB_ENV | |
| shell: bash | |
| - name: Check diff for unicode | |
| continue-on-error: true | |
| id: unicode_diff | |
| run: | | |
| set -x | |
| git config --global --add safe.directory . | |
| git config --global --add safe.directory "$(pwd)" | |
| git branch -a | |
| git log | |
| git fetch origin refs/pull/${{ github.event.number }}/head:this_pr | |
| git checkout this_pr | |
| git branch -a | |
| git log | |
| diff=`git diff --unified=0 ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -E "^[+]" | grep -Ev '^(--- a/|\+\+\+ b/)'` | |
| if [ $? -ne 0 ]; then | |
| # there was an error in the diff | |
| human_result="WARNING: git diff failed!" | |
| echo "UNICODE_HUMAN_RESULT=${human_result}" >> $GITHUB_ENV | |
| echo "${human_result}" | |
| exit 1 | |
| fi | |
| unicode_diff=`echo -n "${diff}" | grep -oP "[^\x00-\x7F]*"` | |
| unicode_grep_exit_code=$? | |
| echo "${unicode_diff}" | |
| unicode_diff_hexdump=`echo -n "${unicode_diff}" | hd` | |
| if [ $? -ne 0 ]; then | |
| # there was an error in the hexdump | |
| human_result="WARNING: hexdump failed!" | |
| echo "UNICODE_HUMAN_RESULT=${human_result}" >> $GITHUB_ENV | |
| echo "${human_result}" | |
| exit 1 | |
| fi | |
| echo "${unicode_diff_hexdump}" | |
| # did we select any unicode characters? | |
| if [[ "${unicode_diff_hexdump}" == "" ]]; then | |
| # we didn't find any unicode characters | |
| human_result="INFO: No unicode characters found in PR's commits" | |
| echo "${human_result}" | |
| else | |
| # we found at least 1 unicode character | |
| human_result="^^ WARNING: Unicode characters found in diff!" | |
| echo "${human_result}" | |
| echo "${diff}" | |
| fi | |
| echo "UNICODE_HUMAN_RESULT=${human_result}" >> $GITHUB_ENV | |
| shell: bash {0} | |
| # leave a comment on the PR. See also | |
| # * https://stackoverflow.com/a/64126737 | |
| # make sure this doesn't open command injection risks | |
| # * https://github.com/victoriadrake/github-guestbook/issues/1#issuecomment-657121754 | |
| - name: Leave comment on PR | |
| uses: actions/github-script@v5 | |
| with: | |
| github-token: ${{secrets.GITHUB_TOKEN}} | |
| script: | | |
| github.rest.issues.createComment({ | |
| issue_number: context.issue.number, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| body: "${{ env.UNICODE_HUMAN_RESULT }}\n\n([source](${{ env.RUN_URL }}))" | |
| }) | |
| # Exit with or without error | |
| - name: Exit with or without error | |
| run: | | |
| if [[ $(echo "${{ env.UNICODE_HUMAN_RESULT }}" | grep -Ei "ERROR|WARNING") ]]; then | |
| exit 1 | |
| else | |
| exit 0 | |
| shell: bash {0} |