github: use gitlint config from sel4_tools

Previously, gitlint would use the configuration from the local
repository only.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein
2020-05-12 09:22:26 +08:00
parent 13d1a9963b
commit a4b1e347f6

View File

@@ -16,13 +16,17 @@ jobs:
fetch-depth: 2
- run: |
git fetch --depth 1 --no-tags origin +refs/heads/${{ github.base_ref }}:refs/heads/${{ github.base_ref }}
- uses: actions/checkout@v2
with:
repository: seL4/sel4_tools
path: sel4_tools
- uses: actions/setup-python@v1
with:
python-version: '3.7'
- name: Install gitlint
run: pip install gitlint
- name: Run gitlint
run: gitlint --commits ${{ github.base_ref }}..${{ github.event.pull_request.head.sha }} lint
run: gitlint --commits ${{ github.base_ref }}..${{ github.event.pull_request.head.sha }} --config sel4_tools/misc/.gitlint lint
whitespace:
name: Trailing Whitespace