2 Commits

Author SHA1 Message Date
f07abaff3a ci: Set file mtimes from git log
All checks were successful
infra/kickstart/pipeline/head This commit looks good
Every time the job runs, the _Publish_ stage changes the timestamps of
the files on the server, even if their contents haven't changed.  This
is because each build runs from a fresh checkout, so every file appears
to have just been created.  To avoid this, and leave files on the server
alone unless they've changed, we now set the modification timestamp of
every file from its last commit.
2025-07-09 10:39:10 -05:00
06ffb6713c ci: Add Jenkins build+publish pipeline 2025-07-09 10:25:47 -05:00