Menu ▾ ▴

#3547 jedit script should use ${JAVA_HOME}

minor bug
closed-fixed
Björn Kautler
None
5
2011-06-28
2011-06-21
Ben Golding
No

Bug in launcher shell script (Linux only affected).

$JAVA_HOME should be ${JAVA_HOME} (2 instances)
$DEFAULT_JAVA_HOME should be ${DEFAULT_JAVA_HOME}

I believe this is in line with best practices and avoids a potential issue if the user sets e.g. $JAVA or $DEFAULT

-----
jEdit 4.4.1
Java(TM) SE Runtime Environment (build 1.6.0_26-b03)
RedHat Enterprise Linux 4.0 U8

Discussion

  • Björn Kautler

    Björn Kautler - 2011-06-28
    • labels: 103010 -->
    • assigned_to: shlomy --> vampire0
    • status: open --> closed-fixed
     

  • Björn Kautler

    Björn Kautler - 2011-06-28

    Hi Ben,

    if a user sets $JAVA this doesn't influence the script at all (just tried it to be sure).
    The problem if not using {} is the other way around, like further down in the jEdit launch script.
    If you write "-Xmx$JAVA_HEAP_MAX_SIZEM" bash searches for JAVA_HEAP_MAX_SIZEM and no substring of it, that is why there {} are used and it actually is "-Xmx${JAVA_HEAP_MAX_SIZE}M".

    But just in case there are other shells that behave differently I changed the usages to include the {}.
    Anyway thanks for your report which just made me see that the Java installer actually dynamically creates a completely different *nix launcher script than we use usually. I also fixed this now.

     

Log in to post a comment.