Switch the MPS manual to using the Read the Docs theme #416
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
| # .github/workflows/shell-script-check.yml -- check shell scripts | |
| # | |
| # This is a GitHub CI workflow | |
| # <https://docs.github.com/en/actions/using-workflows/about-workflows> | |
| # to check shell scripts. | |
| name: shell script check | |
| on: | |
| # Run as part of CI checks on branch push and on merged pull request. | |
| - push | |
| - pull_request | |
| - workflow_dispatch # allow manual triggering | |
| jobs: | |
| check-shell-scripts: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Install shellcheck | |
| run: sudo apt-get install -y shellcheck | |
| - name: Check shell scripts | |
| run: tool/check-shell-scripts |