# HG changeset patch
# User wenzelm
# Date 1476304691 -7200
# Node ID 8945293a9ed0da7b4490c4103fac721c7611a596
# Parent  54479f7b668552b1bc4be11e5dfc5b89d2f2814b
special case for local contrib, e.g. lxbroy10;

diff -r 54479f7b6685 -r 8945293a9ed0 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"