lib/Tools/getenv
changeset 2296 3b1086cf2f4d
child 2307 508d2a233dbc
equal deleted inserted replaced
2295:bae5683c2891 2296:3b1086cf2f4d
       
     1 #!/bin/bash
       
     2 #
       
     3 # DESCRIPTION: get value from Isabelle settings
       
     4 #
       
     5 
       
     6 PRG=$(basename $0)
       
     7 
       
     8 function usage()
       
     9 {
       
    10   echo
       
    11   echo "Usage: $PRG VARNAME"
       
    12   echo
       
    13   echo "  Get value of VARNAME from the Isabelle settings."
       
    14   echo
       
    15   exit 1
       
    16 }
       
    17 
       
    18 
       
    19 ## main
       
    20 
       
    21 [ $# -ne 1 ] && usage
       
    22 
       
    23 eval "echo \$$1"