Scopes: Initial draft of scope structure and decoding #72
This file contains hidden or 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
| name: CI | |
| on: | |
| pull_request_target: | |
| types: [opened, reopened, synchronize] | |
| push: | |
| branches-ignore: | |
| - 'gh-pages' | |
| jobs: | |
| build: | |
| name: Build and Validate | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v3 | |
| - run: npm ci | |
| # SECURITY: We only checkout spec.emu and img/ from the PR because | |
| # we need to make sure that a PR cannot steal the GITHUB_TOKEN | |
| # by modifying scripts that run during the various npm commands. | |
| # Given that we are using `pull_request_target`, GITHUB_TOKEN will | |
| # have write permissions to the repo. | |
| # With `pull_request_target`, the code in the PR should be considered | |
| # to be pure "data" to process, rather than runnable code. See | |
| # https://securitylab.github.com/resources/github-actions-preventing-pwn-requests/ | |
| - name: Checkout spec from PR | |
| if: github.event_name != 'push' | |
| run: | | |
| git fetch origin +refs/pull/${{ github.event.pull_request.number }}/head | |
| git checkout FETCH_HEAD -- spec.emu img/ | |
| - run: npm run build | |
| - run: npx emu-format --check spec.emu | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: out/ | |
| deploy: | |
| name: Deploy | |
| needs: build | |
| permissions: | |
| contents: write | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| ref: gh-pages | |
| - uses: actions/download-artifact@v4 | |
| if: success() || failure() | |
| - run: cp -r ./artifact/. . | |
| if: github.event_name == 'push' && github.ref_name == 'main' | |
| - run: mkdir -p branch && cp -r ./artifact/. ./branch/${{ github.ref_name }} | |
| if: github.event_name == 'push' && github.ref_name != 'main' | |
| - run: mkdir -p pr && cp -r ./artifact/. ./pr/${{ github.event.number }} | |
| if: github.event_name != 'push' | |
| - run: rm -r artifact | |
| - name: Configure git | |
| run: | | |
| git config user.email "41898282+github-actions[bot]@users.noreply.github.com" | |
| git config user.name "github-actions[bot]" | |
| - name: Push to gh-pages | |
| run: | | |
| git add . | |
| git commit -m "Deploy ${{ github.event_name }} ${{ github.ref_name }}" --allow-empty | |
| git push |