From 5d207fff9279f2e70f5b2dd600286a5c1591dd11 Mon Sep 17 00:00:00 2001
From: Philipp Spilger <philipp.spilger@kip.uni-heidelberg.de>
Date: Tue, 24 Oct 2023 10:51:08 +0200
Subject: [PATCH] chore: use updated build cache
Change-Id: I54bdd01e96bb36bfe760da22bcc2c381ef00bc73
---
.ci/Jenkinsfile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile
index 90520fe2..f1e4ebf8 100755
--- a/.ci/Jenkinsfile
+++ b/.ci/Jenkinsfile
@@ -23,7 +23,7 @@ pipeline {
parameters {
string(name: 'BUILD_CACHE_NAME',
- defaultValue: 'init_from_2023-09-07_1',
+ defaultValue: 'init_from_2023-10-24',
description: 'Which buildcache to use? They reside under $HOME/build_caches/$BUILD_CACHE_NAME and will be created if they do not exist.')
}
--
GitLab