clarified permissions;
authorwenzelm
Wed, 22 Apr 2015 20:16:28 +0200
changeset 60191 46a353f6aa39
parent 60190 906de96ba68a
child 60192 39a2f9209a80
clarified permissions;
Admin/Release/build_library
--- a/Admin/Release/build_library	Wed Apr 22 20:14:43 2015 +0200
+++ b/Admin/Release/build_library	Wed Apr 22 20:16:28 2015 +0200
@@ -87,6 +87,7 @@
 cd ..
 
 if [ "$RC" = 0 ]; then
+  chmod -R a+r "$ISABELLE_NAME"
   chmod -R g=o "$ISABELLE_NAME"
   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
 fi