equal
deleted
inserted
replaced
32 function jvmpath() { echo "$@"; } |
32 function jvmpath() { echo "$@"; } |
33 CLASSPATH="$CLASSPATH" |
33 CLASSPATH="$CLASSPATH" |
34 fi |
34 fi |
35 |
35 |
36 export ISABELLE_HOME |
36 export ISABELLE_HOME |
37 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } |
|
38 then |
|
39 echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!" |
|
40 echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\"" |
|
41 fi |
|
42 |
37 |
43 #key executables |
38 #key executables |
44 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process" |
39 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process" |
45 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
40 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
46 |
41 |
56 exit 2 |
51 exit 2 |
57 fi |
52 fi |
58 |
53 |
59 #Isabelle distribution identifier -- filled in automatically! |
54 #Isabelle distribution identifier -- filled in automatically! |
60 ISABELLE_ID="" |
55 ISABELLE_ID="" |
61 ISABELLE_IDENTIFIER="" |
56 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" |
62 |
57 |
63 #sometimes users put strange things in here ... |
58 #sometimes users put strange things in here ... |
64 unset ENV |
59 unset ENV |
65 unset BASH_ENV |
60 unset BASH_ENV |
66 |
61 |