lib/Tools/getenv
author wenzelm
Mon Dec 02 18:19:50 1996 +0100 (1996-12-02)
changeset 2296 3b1086cf2f4d
child 2307 508d2a233dbc
permissions -rwxr-xr-x
getenv: get value from Isabelle settings.
     1 #!/bin/bash
     2 #
     3 # DESCRIPTION: get value from Isabelle settings
     4 #
     5 
     6 PRG=$(basename $0)
     7 
     8 function usage()
     9 {
    10   echo
    11   echo "Usage: $PRG VARNAME"
    12   echo
    13   echo "  Get value of VARNAME from the Isabelle settings."
    14   echo
    15   exit 1
    16 }
    17 
    18 
    19 ## main
    20 
    21 [ $# -ne 1 ] && usage
    22 
    23 eval "echo \$$1"