lib/scripts/getsettings
changeset 2307 508d2a233dbc
parent 2299 ed9720047d53
child 2348 b51e104ecf40
     1.1 --- a/lib/scripts/getsettings	Wed Dec 04 12:30:49 1996 +0100
     1.2 +++ b/lib/scripts/getsettings	Wed Dec 04 13:05:47 1996 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 +#
     1.5 +# $Id$
     1.6  #
     1.7  # getsettings - bash source script to augment current env
     1.8  #
     1.9 -# $Id$
    1.10 -#
    1.11  
    1.12  #value set by caller
    1.13  export ISABELLE_HOME