linux launcher: use thirdpary JVM when DEVTOOLS are available 84/21284/1
Clément DAVID [Wed, 5 Feb 2020 17:18:23 +0000 (18:18 +0100)]
Change-Id: I1fbc6c71da073b6bbcc0958c5ff14bc36e2ef05c

scilab/bin/scilab

index f553e82..978f712 100755 (executable)
@@ -442,6 +442,15 @@ detect_java_vm() {
                     echo "Cannot find $JAVA_HOME/bin/java"
                     exit 1
                 fi
+        elif test "$DEVENV" -eq 1 -a -d "$SCI/java/jre" ; then
+                export JAVA_HOME=$SCI/java/jre
+                if test $SCIVERBOSE -ne 0; then
+                    echo "Using thirdparty vm: $JAVA_HOME"
+                fi
+                if test ! -x "$JAVA_HOME/bin/java" ; then
+                    echo "Cannot find $JAVA_HOME/bin/java"
+                    exit 1
+                fi
         else
 
             case $OS in