# HG changeset patch
# User haftmann
# Date 1128410357 -7200
# Node ID f546af04142a45c22f6fdbeea7b292d2d4d1df5c
# Parent  549fe09d27b17473c12703303a60343487408ae8
support for setting local permissions

diff -r 549fe09d27b1 -r f546af04142a Admin/website/README
--- a/Admin/website/README	Tue Oct 04 08:49:24 2005 +0200
+++ b/Admin/website/README	Tue Oct 04 09:19:17 2005 +0200
@@ -113,9 +113,10 @@
 * log in to sunbroy2
 * go to ~/isabelle/website_build
 * there do an CVS update if desired
+* do "make perms" to set file owner group (isabelle) and permissions
+  (rw-rw-r--, rwxrwsr-x)
 * do your changes
 * just type make - the website is builded to the website synchronization cache
-* for sure, check groups (isabelle) and permissions (rw-/rwx)
 * then do CVS commit
 * for updating the webpage in Munich, just use Admin/mirror-website
 * if the Isabelle distribution files themselves change, some handwired updating
diff -r 549fe09d27b1 -r f546af04142a Admin/website/build/localconf.at.template.mak
--- a/Admin/website/build/localconf.at.template.mak	Tue Oct 04 08:49:24 2005 +0200
+++ b/Admin/website/build/localconf.at.template.mak	Tue Oct 04 09:19:17 2005 +0200
@@ -15,9 +15,12 @@
 STATICDIRS=css img media misc
 
 # umask/group for target files
-TARGET_UMASK_FILE=664
-TARGET_UMASK_DIR=775
+TARGET_UMASK_FILE=u=rw,g=rw,o=r
+TARGET_UMASK_DIR=u=rwx,g=rwx,o=rx,g+s
 TARGET_GROUP=isabelle
+LOCAL_UMASK_FILE=u=rw,g=rw,o=r
+LOCAL_UMASK_DIR=u=rwx,g=rwx,o=rx,g+s
+LOCAL_GROUP=isabelle
 
 # python interpreter (>= 2.3)
 PYTHON=python
diff -r 549fe09d27b1 -r f546af04142a Admin/website/build/localconf.sun.template.mak
--- a/Admin/website/build/localconf.sun.template.mak	Tue Oct 04 08:49:24 2005 +0200
+++ b/Admin/website/build/localconf.sun.template.mak	Tue Oct 04 09:19:17 2005 +0200
@@ -15,9 +15,12 @@
 STATICDIRS=css img media misc
 
 # umask/group for target files
-TARGET_UMASK_FILE=664
-TARGET_UMASK_DIR=775
+TARGET_UMASK_FILE=u=rw,g=rw,o=r
+TARGET_UMASK_DIR=u=rwx,g=rwx,o=rx,g+s
 TARGET_GROUP=isabelle
+LOCAL_UMASK_FILE=u=rw,g=rw,o=r
+LOCAL_UMASK_DIR=u=rwx,g=rwx,o=rx,g+s
+LOCAL_GROUP=isabelle
 
 # python interpreter (>= 2.3)
 PYTHON=python2.3
diff -r 549fe09d27b1 -r f546af04142a Admin/website/build/make_dep.bash
--- a/Admin/website/build/make_dep.bash	Tue Oct 04 08:49:24 2005 +0200
+++ b/Admin/website/build/make_dep.bash	Tue Oct 04 09:19:17 2005 +0200
@@ -23,6 +23,7 @@
         echo '	mkdir -p $(dir $@)' >> "$DEP_FILE"
         echo '	-chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE"
         echo '	-chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE"
+        echo '	rm $@' >> "$DEP_FILE"
         echo '	cp $< $@' >> "$DEP_FILE"
         echo '	chmod $(TARGET_UMASK_DIR) $@' >> "$DEP_FILE"
         echo '	chgrp $(TARGET_GROUP) $@' >> "$DEP_FILE"
@@ -42,6 +43,7 @@
     echo '	mkdir -p $(dir $@)' >> "$DEP_FILE"
     echo '	-chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE"
     echo '	-chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE"
+    echo '	rm $@' >> "$DEP_FILE"
     echo '	$(PYTHON) build/pypager.py --dtd="dtd/" $(FORCE_ENC_CMD) --srcroot="." --dstroot="$(OUTPUTROOT)" distname="$(DISTNAME)" $< $@' >> "$DEP_FILE"
     echo '	-$(TIDYCMD) $@' >> "$DEP_FILE"
     echo '	chmod $(TARGET_UMASK_DIR) $@' >> "$DEP_FILE"
diff -r 549fe09d27b1 -r f546af04142a Admin/website/build/project.mak
--- a/Admin/website/build/project.mak	Tue Oct 04 08:49:24 2005 +0200
+++ b/Admin/website/build/project.mak	Tue Oct 04 09:19:17 2005 +0200
@@ -25,3 +25,7 @@
 	echo 'echo "DISTNAME=Isabelle1705" > conf/distname.mak'; \
 	echo; \
 	false; \
+
+perms:
+	build/set_perm.bash $(FIND) $(LOCAL_UMASK_FILE) $(LOCAL_UMASK_DIR) $(LOCAL_GROUP)
+.PHONY: perms
\ No newline at end of file
diff -r 549fe09d27b1 -r f546af04142a Admin/website/build/set_perm.bash
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/set_perm.bash	Tue Oct 04 09:19:17 2005 +0200
@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# $Id$
+
+# set permissions for local files
+
+# parameters
+FIND="$1"
+LOCAL_UMASK_FILE="$2"
+LOCAL_UMASK_DIR="$3"
+LOCAL_GROUP="$4"
+
+for file in $("$FIND" .)
+do
+    if [ -O "$file" ]
+    then
+        echo "$file..."
+        if [ -d "$file" ]
+        then
+            chmod "$LOCAL_UMASK_DIR" "$file"
+        else
+            if [ -x "$file" ]
+            then
+                chmod "$LOCAL_UMASK_FILE",u+x,g+x,o+x "$file"
+            else
+                chmod "$LOCAL_UMASK_FILE" "$file"
+            fi
+        fi
+    fi
+done