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
Tue, 17 Dec 1996 12:51:54 +0100
changeset 2428 853732a26bdd
parent 2348 b51e104ecf40
child 2478 adbd622bb375
permissions -rw-r--r--
improved error handling;
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
 
#
2348
b51e104ecf40 *** empty log message ***
wenzelm
parents: 2307
diff changeset 
     4
 
# getsettings - bash source script to augment current env.
2299
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









2428






853732a26bdd
improved error handling;



wenzelm


parents: 
2348

diff
changeset




    12


. $ISABELLE_HOME/etc/settings || exit 2








2299






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