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
Thu, 23 Jan 1997 18:10:29 +0100
changeset 2548 b5d19d99a58d
parent 2478 adbd622bb375
child 2590 363b2c37a1b9
permissions -rw-r--r--
'rm -f' instead of 'cp -f';
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









2478






adbd622bb375
added ISABELLE, ISATOOL;



wenzelm


parents: 
2428

diff
changeset




    15


ISABELLE=$ISABELLE_HOME/bin/isabelle













adbd622bb375
added ISABELLE, ISATOOL;



wenzelm


parents: 
2428

diff
changeset




    16


ISATOOL=$ISABELLE_HOME/bin/isatool













adbd622bb375
added ISABELLE, ISATOOL;



wenzelm


parents: 
2428

diff
changeset




    17









2299






ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    18


set +o allexport















isabelle