build-docs.jpl: Replace old docs with newly generated
Instead of just overlaying new files over the old directory, with old file
(and links) remaing active and causing confusion. Do the replace in as
atomic way as possible, to avoid users getting non-deterministic 404 HTTP
errors.
Signed-off-by: Paul Sokolovsky <paul.sokolovsky@linaro.org>
Change-Id: I14be7522ef6f7b78484d2fe6c517fa0064898456
diff --git a/jenkins/build-docs.jpl b/jenkins/build-docs.jpl
index aa8bc65..bf892d1 100644
--- a/jenkins/build-docs.jpl
+++ b/jenkins/build-docs.jpl
@@ -43,9 +43,15 @@
}
node("master") {
if (env.JOB_NAME.equals("tf-m-build-docs-nightly")) {
+ // Copy, then as atomically as possible replace previous docs with new.
sh """
- cp -a /var/jenkins_home/jobs/$JOB_NAME/builds/$BUILD_NUMBER/archive/trusted-firmware-m/build/docs/reference_manual /var/jenkins_home/docs/
- cp -a /var/jenkins_home/jobs/$JOB_NAME/builds/$BUILD_NUMBER/archive/trusted-firmware-m/build/docs/user_guide /var/jenkins_home/docs/
+ cp -a /var/jenkins_home/jobs/$JOB_NAME/builds/$BUILD_NUMBER/archive/trusted-firmware-m/build/docs/reference_manual /var/jenkins_home/docs/reference_manual.new
+ cp -a /var/jenkins_home/jobs/$JOB_NAME/builds/$BUILD_NUMBER/archive/trusted-firmware-m/build/docs/user_guide /var/jenkins_home/docs/user_guide.new
+ rm -rf /var/jenkins_home/docs/reference_manual.old /var/jenkins_home/docs/user_guide.old
+ mv /var/jenkins_home/docs/reference_manual /var/jenkins_home/docs/reference_manual.old
+ mv /var/jenkins_home/docs/user_guide /var/jenkins_home/docs/user_guide.old
+ mv /var/jenkins_home/docs/reference_manual.new /var/jenkins_home/docs/reference_manual
+ mv /var/jenkins_home/docs/user_guide.new /var/jenkins_home/docs/user_guide
"""
}
}