From 4ba1417f54fa7652c5851e0a96485d991acdc6ff Mon Sep 17 00:00:00 2001
From: Martin Robertz <dream-master@gmx.net>
Date: Sun, 3 Dec 2023 21:36:14 +0100
Subject: update gradle+bs+deps

---
 gradlew | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'gradlew')

diff --git a/gradlew b/gradlew
index aeb74cbb43..fcb6fca147 100755
--- a/gradlew
+++ b/gradlew
@@ -130,10 +130,13 @@ location of your Java installation."
     fi
 else
     JAVACMD=java
-    which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
+    if ! command -v java >/dev/null 2>&1
+    then
+        die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
 
 Please set the JAVA_HOME variable in your environment to match the
 location of your Java installation."
+    fi
 fi
 
 # Increase the maximum file descriptors if we can.
-- 
cgit