Merge PR #9224: Move lint job to gitlab

1 files changed, 10 insertions, 18 deletions

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index cd09b6d305..f588c20d02 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -4,33 +4,25 @@
 
 # lint-commits.sh seeks to prevent the worsening of already present
 # problems, such as tab indentation in ml files. lint-repository.sh
-# seeks to prevent the (re-)introduction of solved problems, such as
-# newlines at the end of .v files.
+# also seeks to prevent the (re-)introduction of solved problems, such
+# as newlines at the end of .v files.
 
 CODE=0
 
-if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
-then
-    # skip PRs from before the linter existed
-    if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
-    then
-        1>&2 echo "Linting skipped: pull request older than the linter."
-        exit 0
-    fi
-
-    # Some problems are too widespread to fix in one commit, but we
-    # can still check that they don't worsen.
-    CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
-    PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
-    MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD")
-    dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1
-fi
+# We assume that all merge commits are from the main branch
+# For Coq it is extremely rare for this assumption to be broken
+read -r base < <(git log -n 1 --merges --pretty='format:%H')
+head=$(git rev-parse HEAD)
+
+dev/lint-commits.sh "$base" "$head" || CODE=1
 
 # Check that the files with 'whitespace' gitattribute end in a newline.
 # xargs exit status is 123 if any file failed the test
+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
 
 exit $CODE