ci: Set file mtimes from git log

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.

.rsync-filter

@@ -3,5 +3,6 @@
 - *.j2
 - .gitignore
 - Makefile
+- fixtimes.sh
 - publish.sh
 - render.py

ci/Jenkinsfile

@@ -10,6 +10,7 @@ pipeline {
     stages {
         stage('Build') {
             steps {
+                sh './fixtimes.sh'
                 sh 'make'
             }
         }

fixtimes.sh

@@ -0,0 +1,8 @@
+#!/bin/sh
+
+git ls-files | while IFS= read -r file; do
+    ts=$(git log -1 --format=%at -- "${file}")
+    if [ -n "${ts}" ]; then
+        touch -d "@${ts}" -- "${file}"
+    fi
+done