fix CI on push

for reference, documentation is here:
ttps://docs.github.com/en/actions/learn-github-actions/contexts#github-context
This commit is contained in:
Pierre Chapuis 2024-01-08 09:38:55 +01:00
parent 00f494efe2
commit a08e04c5af

View file

@ -7,7 +7,7 @@ on:
jobs: jobs:
lint_and_typecheck: lint_and_typecheck:
if: ${{ github.event.name == 'push' || github.event.label.name == 'run-ci' }} if: ${{ github.event_name == 'push' || github.event.label.name == 'run-ci' }}
runs-on: ubuntu-latest runs-on: ubuntu-latest
steps: steps: