lib/Tools/getenv
author wenzelm
Mon Dec 09 09:04:07 1996 +0100 (1996-12-09)
changeset 2335 e965156e84e3
parent 2307 508d2a233dbc
child 2733 1d1013313201
permissions -rwxr-xr-x
added -norc option;
     1 #!/bin/bash -norc
     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"