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
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 6413 b2f2770ef8d9
child 7770 0497323c1f0b
permissions -rw-r--r--
tuned;
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
 







3185





wenzelm


parents: 
3118

diff
changeset




     7


set -o allexport












wenzelm


parents: 
3118

diff
changeset




     8









2736






476adc742599
added ISABELLE_HOME normalization;



wenzelm


parents: 
2643

diff
changeset




     9


#normalize ISABELLE_HOME as passed by caller













476adc742599
added ISABELLE_HOME normalization;



wenzelm


parents: 
2643

diff
changeset




    10


ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)













476adc742599
added ISABELLE_HOME normalization;



wenzelm


parents: 
2643

diff
changeset




    11









3185





wenzelm


parents: 
3118

diff
changeset




    12


#main executables












wenzelm


parents: 
3118

diff
changeset




    13


ISABELLE=$ISABELLE_HOME/bin/isabelle












wenzelm


parents: 
3118

diff
changeset




    14


ISATOOL=$ISABELLE_HOME/bin/isatool








2299






ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    15









2643






a7f469c0ba59
tuned comments;



wenzelm


parents: 
2621

diff
changeset




    16


#users tend to put strange things in here ...








2621






e9e491033b54
globally unset ENV, BASH_ENV;



wenzelm


parents: 
2590

diff
changeset




    17


unset ENV













e9e491033b54
globally unset ENV, BASH_ENV;



wenzelm


parents: 
2590

diff
changeset




    18


unset BASH_ENV













e9e491033b54
globally unset ENV, BASH_ENV;



wenzelm


parents: 
2590

diff
changeset




    19









2643






a7f469c0ba59
tuned comments;



wenzelm


parents: 
2621

diff
changeset




    20


#get actual settings








2428






853732a26bdd
improved error handling;



wenzelm


parents: 
2348

diff
changeset




    21


. $ISABELLE_HOME/etc/settings || exit 2








2299






ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    22


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













ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    23









6413






b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    24


#append ML system identifier to paths













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    25


if [ -z "$ML_PLATFORM" ]; then













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    26


  ML_IDENTIFIER="$ML_SYSTEM"













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    27


else













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    28


  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    29


fi













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    30


ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"













b2f2770ef8d9
ML_PLATFORM;



wenzelm


parents: 
3185

diff
changeset




    31


ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done)








3118






24dae6222579
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);



wenzelm


parents: 
2968

diff
changeset




    32


ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)













24dae6222579
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);



wenzelm


parents: 
2968

diff
changeset




    33









2299






ed9720047d53
getsettings: bash source script to augment current env.



wenzelm


parents: 

diff
changeset




    34


set +o allexport















isabelle