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;
wenzelm@2335
     1
#!/bin/bash -norc
wenzelm@2296
     2
#
wenzelm@2307
     3
# $Id$
wenzelm@2307
     4
#
wenzelm@2296
     5
# DESCRIPTION: get value from Isabelle settings
wenzelm@2307
     6
wenzelm@2296
     7
wenzelm@2296
     8
PRG=$(basename $0)
wenzelm@2296
     9
wenzelm@2296
    10
function usage()
wenzelm@2296
    11
{
wenzelm@2296
    12
  echo
wenzelm@2296
    13
  echo "Usage: $PRG VARNAME"
wenzelm@2296
    14
  echo
wenzelm@2296
    15
  echo "  Get value of VARNAME from the Isabelle settings."
wenzelm@2296
    16
  echo
wenzelm@2296
    17
  exit 1
wenzelm@2296
    18
}
wenzelm@2296
    19
wenzelm@2296
    20
wenzelm@2296
    21
## main
wenzelm@2296
    22
wenzelm@2296
    23
[ $# -ne 1 ] && usage
wenzelm@2296
    24
wenzelm@2296
    25
eval "echo \$$1"