diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 18:24:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 18:24:19 +0100 |
| commit | 1dbb4e77051324e229f7006161746030e5369565 (patch) | |
| tree | 85d80eae8d8fdf1ddb738acf953130922c1f8916 /dev | |
| parent | e7d970b22512b31db96f9a06e5319b4af696d1b5 (diff) | |
| parent | 136b61ae70113922330de032f005b4acb50bc800 (diff) | |
Merge PR #9592: Fix per-commit linting with bot merges
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-repository.sh | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index f588c20d02..2e8a7455de 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,17 @@ CODE=0 -# We assume that all merge commits are from the main branch +if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then + # The FIRST parent of bot merges is from the PR, the second is + # current master + head=$(git rev-parse HEAD~) +else + head=$(git rev-parse HEAD) +fi + +# We assume that all non-bot 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) +read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head") dev/lint-commits.sh "$base" "$head" || CODE=1 |