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