# HG changeset patch
# User wenzelm
# Date 1441887489 -7200
# Node ID 9005aeb8125a4e038cdeaa751176b9a0161b5798
# Parent  d85d8f5e921b57b8510c462b6e596d98c32c91b8
convenient access to application properties;

diff -r d85d8f5e921b -r 9005aeb8125a Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Thu Sep 10 14:12:22 2015 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Thu Sep 10 14:18:09 2015 +0200
@@ -381,6 +381,7 @@
           chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
 
         mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
+        ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist"
         ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
 
         rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"