special case for local contrib, e.g. lxbroy10;
authorwenzelm
Wed, 12 Oct 2016 22:38:11 +0200
changeset 64175 8945293a9ed0
parent 64174 54479f7b6685
child 64176 35644caa62a7
special case for local contrib, e.g. lxbroy10;
Admin/lib/Tools/makedist_bundle
--- 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"