changeset 64175 | 8945293a9ed0 |
parent 64147 | 92066f8c6a54 |
child 64176 | 35644caa62a7 |
--- a/Admin/lib/Tools/makedist_bundle Wed Oct 12 22:06:06 2016 +0200 +++ b/Admin/lib/Tools/makedist_bundle Wed Oct 12 22:38:11 2016 +0200 @@ -71,6 +71,7 @@ ENTRY=$(echo "$ENTRY" | perl -n -e " if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; } elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } + elsif (m,/home/isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } else { print; }; print qq{\n};") DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY"