mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
Run super-linter in all branches
Use the same trigger as in the rest of jobs. Before submitting a PR, commit is pushed to a private branch where the jobs are executed. Super-linter should be executed in these jobs as well to get signal about linting issue before submitting a PR, to reduce noise to PR reviewers.
This commit is contained in:
parent
5720d1c691
commit
cffade6bf8
12
.github/workflows/ci-super-linter.yml
vendored
12
.github/workflows/ci-super-linter.yml
vendored
@ -11,15 +11,15 @@ name: Lint Code Base
|
||||
# https://help.github.com/en/articles/workflow-syntax-for-github-actions
|
||||
#
|
||||
|
||||
#############################
|
||||
# Start the job on all push #
|
||||
#############################
|
||||
on:
|
||||
push:
|
||||
# branches-ignore: [master]
|
||||
# Remove the line above to run when pushing to master
|
||||
branches:
|
||||
- '*'
|
||||
tags:
|
||||
- '*'
|
||||
pull_request:
|
||||
branches: [master]
|
||||
branches:
|
||||
- master
|
||||
|
||||
###############
|
||||
# Set the Job #
|
||||
|
Loading…
Reference in New Issue
Block a user