[CI] Retrieve lint job

coq · Sep 16, 2024 · 20383b1 · 20383b1
1 parent bc8ace3
commit 20383b1
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 11 deletions.
diff --git a/.github/workflows/basic-checks.yml b/.github/workflows/basic-checks.yml
@@ -10,7 +10,11 @@ jobs:
     steps:
     - name: Checkout
       uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
     - name: Check consistency of files in Makefiles
       run: dev/tools/check-make-sync.sh
     - name: Check for duplicate files
       run: dev/tools/check-duplicate-files.sh
+    - name: Lint
+      run: dev/lint-repository.sh
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
@@ -48,7 +48,7 @@ while IFS= read -r commit; do
     then bad_ws+=("$commit")
     fi
 
-    if ! make check
+    if ! make
     then bad_compile+=("$commit")
     fi
 done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
@@ -39,14 +39,4 @@ echo Checking end of file newlines
 find . "(" -path ./.git -prune ")" -o -type f -print0 |
     xargs -0 dev/tools/check-eof-newline.sh || CODE=1
 
-echo Checking overlays
-dev/tools/check-overlays.sh || CODE=1
-
-echo Checking CACHEKEY
-dev/tools/check-cachekey.sh || CODE=1
-
-# Check that doc/tools/docgram/fullGrammar is up-to-date
-echo Checking grammar files
-make SHOW='@true ""' doc_gram_verify || CODE=1
-
 exit $CODE