Admin/lib/Tools/makedist_bundle
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"