* Only set JAVA to $JAVA_HOME/jre/bin/java if JAVA_HOME is not empty;
-rw-r--r-- 2646 MEDLINE_FIX.patch
-rw-r--r-- 83 build.number
-rw-r--r-- 22416 build.xml
-rw-r--r-- 2466 changelog_highlights.txt
drwxr-xr-x - debian
-rw-r--r-- 26999 hs_err_pid7783.log
-rw-r--r-- 430 jabref
drwxr-xr-x - lib
drwxr-xr-x - src