From 8ad4513e4745139f3beef0c97d43e4c3a83bf4f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Eric=20M=C3=BCller?= <mueller@kip.uni-heidelberg.de>
Date: Mon, 28 Nov 2022 16:11:23 +0100
Subject: [PATCH] Update build cache
Change-Id: I56deadac2f311c9a58c0eefaae4a8a9c4b9078a1
---
.ci/Jenkinsfile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile
index 7b0a142a..fb8696e7 100755
--- a/.ci/Jenkinsfile
+++ b/.ci/Jenkinsfile
@@ -23,7 +23,7 @@ pipeline {
parameters {
string(name: 'BUILD_CACHE_NAME',
- defaultValue: 'init_from_2022-06-21_1',
+ defaultValue: 'init_from_2022-11-28_1',
description: 'Which buildcache to use? They reside under $HOME/build_caches/$BUILD_CACHE_NAME and will be created if they do not exist.')
}
--
GitLab