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