diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-30 23:34:31 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-30 21:34:31 +0000 |
| commit | 46c994963ef764101409d55d77e0e15db704827b (patch) | |
| tree | 204d701a24812c5f65a30bcc89a631b0b6611d0a /src/prop/minisat/minisat.cpp | |
| parent | a1297ed93895f7405923d6d9e84432767a8abaae (diff) | |
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.
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
0 files changed, 0 insertions, 0 deletions