lib/Tools/getenv
author paulson
Fri, 31 Jan 1997 17:15:55 +0100
changeset 2573 f3e04805895a
parent 2335 e965156e84e3
child 2733 1d1013313201
permissions -rwxr-xr-x
Correction to Problem 24 (with unsatisfactory proof)

#!/bin/bash -norc
#
# $Id$
#
# DESCRIPTION: get value from Isabelle settings


PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG VARNAME"
  echo
  echo "  Get value of VARNAME from the Isabelle settings."
  echo
  exit 1
}


## main

[ $# -ne 1 ] && usage

eval "echo \$$1"