From 2fcc5942da8416113ccda360f3b568991acf567e Mon Sep 17 00:00:00 2001
From: Mathieu <mbaudier@argeo.org>
Date: Fri, 10 Mar 2023 11:01:36 +0100
Subject: [PATCH] Clarify which JAVA_HOME is used by configure

---
 configure | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure b/configure
index 5f28c8a..5d3e45e 100755
--- a/configure
+++ b/configure
@@ -16,8 +16,8 @@ else
 
 if [ -z "$JAVA_HOME" ]
 then
-JAVA_HOME=$(dirname $(dirname $(readlink -f $(which javac))))
-echo "Environment variable JAVA_HOME not set, using $JAVA_HOME"
+JAVA_HOME=$(dirname $(dirname $(readlink -f $(which java))))
+echo "Environment variable JAVA_HOME not set, using $JAVA_HOME of $(which java)"
 fi
 
 # Create build directory, so that it can be used right away
-- 
2.30.2