Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/scripts/getsettings
author wenzelm
Wed, 04 Dec 1996 13:05:47 +0100
changeset 2307 508d2a233dbc
parent 2299 ed9720047d53
child 2348 b51e104ecf40
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2299
diff changeset 
     1
 
#
508d2a233dbc *** empty log message ***
wenzelm
parents: 2299
diff changeset 
     2
 
# $Id$
2299
ed9720047d53 getsettings: bash source script to augment current env.
wenzelm
parents:
diff changeset 
     3
 
#
ed9720047d53 getsettings: bash source script to augment current env.
wenzelm
parents:
diff changeset 
     4
 
# getsettings - bash source script to augment current env
ed9720047d53 getsettings: bash source script to augment current env.
wenzelm
parents:
diff changeset 
     5
 
#
ed9720047d53 getsettings: bash source script to augment current env.
wenzelm
parents:
diff changeset 
     6
 












ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




     7


#value set by caller













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




     8


export ISABELLE_HOME













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




     9














ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    10


set -o allexport













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    11














ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    12


. $ISABELLE_HOME/etc/settings













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    13


[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    14














ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    15


set +o allexport















isabelle