diff --git a/ci/Jenkinsfile b/ci/Jenkinsfile index cefdad6..24ed5aa 100644 --- a/ci/Jenkinsfile +++ b/ci/Jenkinsfile @@ -10,6 +10,7 @@ pipeline { stages { stage('Build') { steps { + sh './fixtimes.sh' sh 'make' } } diff --git a/fixtimes.sh b/fixtimes.sh new file mode 100755 index 0000000..658d7b4 --- /dev/null +++ b/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