Admin/website/build/project.mak
changeset 18214 857444b28267
parent 17949 0150d6d7728b
child 19331 f5e84acd7d3f
equal deleted inserted replaced
18213:c22ee06ac1a7 18214:857444b28267
    18 
    18 
    19 $(OUTPUTROOT)/dist: $(ISABELLE_DIST)
    19 $(OUTPUTROOT)/dist: $(ISABELLE_DIST)
    20 	mkdir -p $@
    20 	mkdir -p $@
    21 	$(COPY) -vRud $</[^w]* $@
    21 	$(COPY) -vRud $</[^w]* $@
    22 	-chgrp -hR $(TARGET_GROUP) $@
    22 	-chgrp -hR $(TARGET_GROUP) $@
    23 	-chmod -R u-w,g-w,o-w $@
    23 	-chmod -R u+w,g-w,o-w $@
    24 	-[ ! -e Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
    24 	-[ ! -e $@/Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
    25 	-chgrp -h $(TARGET_GROUP) $@/Isabelle
    25 	-chgrp -h $(TARGET_GROUP) $@/Isabelle
    26 	-chmod u-w,g-w,o-w $@/Isabelle
    26 	-chmod u+w,g-w,o-w $@/Isabelle
    27 
    27 
    28 else
    28 else
    29 
    29 
    30 $(OUTPUTROOT)/dist: $(ISABELLE_DIST) SYNC_ALWAYS
    30 $(OUTPUTROOT)/dist: $(ISABELLE_DIST) SYNC_ALWAYS
    31 	mkdir -p $@
    31 	mkdir -p $@
    32 	$(RSYNC) -v --exclude='/website/' -rltgoD --delete --delete-after $</ $@
    32 	$(RSYNC) -v --exclude='/website/' -rlt --delete --delete-after $</ $@
    33 	-chgrp -hR $(TARGET_GROUP) $@
    33 	-chgrp -hR $(TARGET_GROUP) $@
    34 	-chmod -R u-w,g-w,o-w $@
    34 	-chmod -R u+w,g-w,o-w $@
    35 	-[ ! -e Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
    35 	-[ ! -e $@/Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
    36 	-chgrp -h $(TARGET_GROUP) $@/Isabelle
    36 	-chgrp -h $(TARGET_GROUP) $@/Isabelle
    37 	-chmod u-w,g-w,o-w $@/Isabelle
    37 	-chmod u+w,g-w,o-w $@/Isabelle
    38 
    38 
    39 SYNC_ALWAYS:
    39 SYNC_ALWAYS:
    40 
    40 
    41 endif
    41 endif
    42 
    42