src/Tools/JVM/java_ext_dirs
changeset 48915 34fac6fb9b03
parent 48914 51560e392e1b
child 48916 f45ccc0d1ace
equal deleted inserted replaced
48914:51560e392e1b 48915:34fac6fb9b03
     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 isabelle_jdk java -Dfile.encoding=UTF-8 \
       
    21   -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
       
    22   isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
       
    23