equal
deleted
inserted
replaced
69 for ENTRY in "${CLASSPATH_ENTRIES[@]}" |
69 for ENTRY in "${CLASSPATH_ENTRIES[@]}" |
70 do |
70 do |
71 ENTRY=$(echo "$ENTRY" | perl -n -e " |
71 ENTRY=$(echo "$ENTRY" | perl -n -e " |
72 if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; } |
72 if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; } |
73 elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } |
73 elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } |
|
74 elsif (m,/home/isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } |
74 else { print; }; |
75 else { print; }; |
75 print qq{\n};") |
76 print qq{\n};") |
76 DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY" |
77 DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY" |
77 done |
78 done |
78 |
79 |