lib/Tools/getenv
changeset 2307 508d2a233dbc
parent 2296 3b1086cf2f4d
child 2335 e965156e84e3
equal deleted inserted replaced
2306:0aadfaf8557a 2307:508d2a233dbc
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
       
     3 # $Id$
       
     4 #
     3 # DESCRIPTION: get value from Isabelle settings
     5 # DESCRIPTION: get value from Isabelle settings
     4 #
     6 
     5 
     7 
     6 PRG=$(basename $0)
     8 PRG=$(basename $0)
     7 
     9 
     8 function usage()
    10 function usage()
     9 {
    11 {