Skip to content

gaplint-73 docs: Add release-badge #28

gaplint-73 docs: Add release-badge

gaplint-73 docs: Add release-badge #28

---
name: gaplint
run-name: gaplint-${{ github.event.number }} ${{ github.event.pull_request.title }}
on:
pull_request:
branches:
- main
jobs:
gaplint:
runs-on: ubuntu-22.04
steps:
- name: git -- checkout
uses: actions/checkout@v4
- name: python -- setup
uses: actions/setup-python@v5
with:
python-version: 3.12
cache: pip
- name: python -- install dependencies
uses: py-actions/py-dependency-install@v4
with:
update-pip: true
- name: gaplint - lint
run: |
echo "::group:: gaplint -- *.g"
find . -name '*.g' | xargs -n1 gaplint
echo "::group:: gaplint -- *.gi"
find . -name '*.gi' | xargs -n1 gaplint
echo "::group:: gaplint -- *.gd"
find . -name '*.gd' | xargs -n1 gaplint
echo "::group:: gaplint -- *.tst"
find . -name '*.tst' | xargs -n1 gaplint