--- a/Admin/website/build/project.mak Fri Oct 21 08:23:45 2005 +0200
+++ b/Admin/website/build/project.mak Fri Oct 21 09:05:52 2005 +0200
@@ -1,6 +1,12 @@
# isaweb makefile - project-specific dependencies
# $Id$
+include conf/distname.mak
+conf/distinfo.mak:
+ @echo 'There is no $@ file; it should have been allocated by makedist.'; \
+ @echo 'If you have no makedist at hand, check out default $@ from CVS'; \
+ @false; \
+
project: $(OUTPUTROOT)/dist site
.PHONY: project
@@ -12,14 +18,14 @@
$(OUTPUTROOT)/dist: $(ISABELLE_DIST)
mkdir -p $@
- $(COPY) -vRud $< $@
+ $(COPY) -vRud $</[^w]* $@
chmod -R g-w $@
else
$(OUTPUTROOT)/dist: $(ISABELLE_DIST) SYNC_ALWAYS
mkdir -p $@
- $(RSYNC) -v -a --delete --delete-after $</ $@
+ $(RSYNC) -v --exclude='/website/' -a --delete --delete-after $</ $@
chmod -R g-w $@
SYNC_ALWAYS:
@@ -29,17 +35,6 @@
include/documentationdist.include.html: $(ISABELLE_DOC_CONTENT_FILE)
perl build/mkcontents.pl -p '//dist/Isabelle/doc/' $< $@
-include conf/distname.mak
-conf/distname.mak:
- @echo 'There is no conf/distname.mak file; it should have been'; \
- echo 'allocated by makedist.'; \
- echo 'If you have no makedist at hand, allocate a conf/distname.mak file'; \
- echo 'yourself, e. g. by:'; \
- echo; \
- 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