diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-09 21:25:04 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-09 19:25:04 +0000 |
| commit | 181a175839e3af50a8cf7f80adf635fe612aeaba (patch) | |
| tree | 4d1fafbff77f02306dae22642b5ee536dbde7cc5 | |
| parent | 2dc245a5922e660b6f44032d55d452ad27dfc20f (diff) | |
Make squasing more robust (#6713)
This PR makes squashing olds commits in the docs-cleanup CI job more robust: it makes sure that the squash commit has a proper commit date and that we gracefully handle if there is nothing to squash.
| -rw-r--r-- | .github/workflows/docs_cleanup.yml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml index 761736e75..6632cbf45 100644 --- a/.github/workflows/docs_cleanup.yml +++ b/.github/workflows/docs_cleanup.yml @@ -44,15 +44,19 @@ jobs: SSH_AUTH_SOCK: /tmp/ssh_agent.sock run: | cd target - git log first=`git rev-list --max-parents=0 HEAD` last=`git rev-list --until=1.month.ago -n1 HEAD` if [ -n "$last" ]; then git checkout $last + ts=`git log -1 --format=%ct` git reset --soft $first - git commit -m "Squash old history" + if git diff --cached --exit-code + then + echo "Nothing to squash" + else + git commit -m "Squash old history" --date=$ts + fi git cherry-pick $last..main - git log fi - name: Push |