lib/Tools/getenv
changeset 3007 e5efa177ee0c
parent 2734 e9bbef1b2fbe
child 9788 df671fa2562a
equal deleted inserted replaced
3006:8a1eb4531fbb 3007:e5efa177ee0c
     1 #!/bin/bash -norc
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: get values from Isabelle settings environment
     5 # DESCRIPTION: get values from Isabelle settings environment
     6 
     6