| changeset 73989 | 842fc354c031 |
| parent 73988 | 678e1c9eb009 |
| child 74017 | b4e6b82fdb9e |
| 73988:678e1c9eb009 | 73989:842fc354c031 |
|---|---|
104 local X="" |
104 local X="" |
105 for X in "$@" |
105 for X in "$@" |
106 do |
106 do |
107 if [ -z "$ISABELLE_CLASSPATH" ]; then |
107 if [ -z "$ISABELLE_CLASSPATH" ]; then |
108 ISABELLE_CLASSPATH="$X" |
108 ISABELLE_CLASSPATH="$X" |
109 else |
109 elif [ -n "$X" ]; then |
110 ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" |
110 ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" |
111 fi |
111 fi |
112 done |
112 done |
113 export ISABELLE_CLASSPATH |
113 export ISABELLE_CLASSPATH |
114 } |
114 } |