From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 30 Jun 2021 21:34:31 +0000 (+0200)
Subject: Use authored date instead of commit date. (#6815)
X-Git-Tag: cvc5-1.0.0~1541
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=46c994963ef764101409d55d77e0e15db704827b;p=cvc5.git

Use authored date instead of commit date. (#6815)

This commit fixes a subtle issue with pruning the old docs from docs-ci. We remove docs that are older than one week. However, we used the commit date instead of the authored date. Since we actually squash the old commits (that are older than four weeks) regularly, the commit date is always newer.
---

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
index 6632cbf45..1bb48ff08 100644
--- a/.github/workflows/docs_cleanup.yml
+++ b/.github/workflows/docs_cleanup.yml
@@ -32,7 +32,7 @@ jobs:
         run: |
           cd target
           for file in `find ./ -maxdepth 1 -name "docs-*"`; do
-            mod=`git log -1 HEAD --pretty="%ci" $file`
+            mod=`git log -1 HEAD --pretty="%ai" $file`
             touch -d "$mod" $file
           done
           find ./ -maxdepth 1 -name "docs-*" -mtime +7 -exec git rm -r {} +