src/Tools/JVM/java_ext_dirs
changeset 45385 7c1375ba1424
parent 43536 6eec653d5599
child 47113 b5a5662528fb
equal deleted inserted replaced
45384:dffa657f0aa2 45385:7c1375ba1424
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Author: Makarius
       
     4 #
       
     5 # Augment Java extension directories.
       
     6 
       
     7 ## diagnostics
       
     8 
       
     9 function fail()
       
    10 {
       
    11   echo "$1" >&2
       
    12   exit 2
       
    13 }
       
    14 
       
    15 [ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
       
    16 
       
    17 
       
    18 ## main
       
    19 
       
    20 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
       
    21 exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
       
    22   isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
       
    23