lib/Tools/java
changeset 27914 9a7f17370ffb
child 27916 09b3010ffaf2
equal deleted inserted replaced
27913:c347986773eb 27914:9a7f17370ffb
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # $Id$
       
     4 # Author: Makarius
       
     5 #
       
     6 # DESCRIPTION: Java wrapper
       
     7 
       
     8 
       
     9 PRG="$(basename "$0")"
       
    10 
       
    11 function usage()
       
    12 {
       
    13   echo
       
    14   echo "Usage: $PRG [ARGS ...]"
       
    15   echo
       
    16   echo "  Invoke Java within the Isabelle environment."
       
    17   echo
       
    18   exit 1
       
    19 }
       
    20 
       
    21 
       
    22 ## main
       
    23 
       
    24 CLASSPATH="$(jvmpath "$CLASSPATH")"
       
    25 exec "$ISABELLE_JAVA" "$@"