From cf35dfc41e9c1b4a5ef646512156e0885f1a5a5c Mon Sep 17 00:00:00 2001
From: Mark Evenson <evenson.not.org@gmail.com>
Date: Wed, 13 Mar 2024 07:38:24 +0100
Subject: [PATCH] ci: jenv doctor exits with non-zero status?

---
 ci/install-openjdk.bash | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ci/install-openjdk.bash b/ci/install-openjdk.bash
index 4fa4b115e..d4635274e 100644
--- a/ci/install-openjdk.bash
+++ b/ci/install-openjdk.bash
@@ -183,3 +183,4 @@ add_jdk_to_jenv
 . ${DIR}/set-jdk.bash ${jdk} ${ABCL_ROOT}
 
 jenv doctor
+exit 0