equal
deleted
inserted
replaced
36 echo |
36 echo |
37 echo " Build object-logic or run examples. Also creates browsing" |
37 echo " Build object-logic or run examples. Also creates browsing" |
38 echo " information (HTML etc.) according to settings." |
38 echo " information (HTML etc.) according to settings." |
39 echo |
39 echo |
40 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
40 echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" |
41 echo " HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS" |
|
42 echo |
41 echo |
43 echo " ML_PLATFORM=$ML_PLATFORM" |
42 echo " ML_PLATFORM=$ML_PLATFORM" |
44 echo " ML_HOME=$ML_HOME" |
43 echo " ML_HOME=$ML_HOME" |
45 echo " ML_SYSTEM=$ML_SYSTEM" |
44 echo " ML_SYSTEM=$ML_SYSTEM" |
46 echo " ML_OPTIONS=$ML_OPTIONS" |
45 echo " ML_OPTIONS=$ML_OPTIONS" |