aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorTej Chajed2020-06-17 13:35:04 -0500
committerTej Chajed2020-06-17 13:35:04 -0500
commit21cc4cb0e687f80e8b49b2a6c9f20331d84d2c39 (patch)
tree7b26b3381659516b5329140286f54f406ffac72d /dev/ci/ci-basic-overlay.sh
parent6499de1a834fa4e039246ac8b821ca23dd2a497e (diff)
[ci] Use a tested branch of Perennial
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index cdf00f4767..475f812b5a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -349,7 +349,7 @@
########################################################################
# perennial
########################################################################
-: "${perennial_CI_REF:=master}"
+: "${perennial_CI_REF:=coq/tested}"
: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"