fix(mypy): ignore type err preventing build (#1991) #5
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: Repo Chores | |
| on: | |
| push: | |
| branches: | |
| - master | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| format: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ github.head_ref }} # Check out the PR branch | |
| - name: Set up Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.13' | |
| - name: Compile | |
| run: pip install . | |
| - name: Check for changes | |
| id: changes | |
| run: | | |
| if [[ -n $(git status --porcelain) ]]; then | |
| echo "changes_detected=true" >> $GITHUB_ENV | |
| else | |
| echo "changes_detected=false" >> $GITHUB_ENV | |
| fi | |
| - name: Commit changes | |
| if: env.changes_detected == 'true' | |
| run: | | |
| git config --local user.name "github-actions[bot]" | |
| git config --local user.email "github-actions[bot]@users.noreply.github.com" | |
| git add . | |
| git commit -m "chore: compile C files for source control" | |
| git push |