[CI] Retrieve lint job

coq · Dec 23, 2024 · 2f4a71b · 2f4a71b
1 parent 20171a3
commit 2f4a71b
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 11 deletions.
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