--- a/Admin/website/build/localconf.at.template.mak Tue Oct 04 08:14:15 2005 +0200
+++ b/Admin/website/build/localconf.at.template.mak Tue Oct 04 08:49:24 2005 +0200
@@ -1,6 +1,24 @@
# isaweb configuration
# $Id$
+# build target (attention: ~ will not work!)
+OUTPUTROOT=$(HOME)/isabelle/website_test
+#~ OUTPUTROOT=/home/proj/isabelle/website
+
+# location of isabelle distribution packages
+ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
+
+# location of doc content file
+ISABELLE_DOC_CONTENT_FILE=$(ISABELLE_DIST)/Isabelle2005/doc/Contents
+
+# dirs to copy to build target
+STATICDIRS=css img media misc
+
+# umask/group for target files
+TARGET_UMASK_FILE=664
+TARGET_UMASK_DIR=775
+TARGET_GROUP=isabelle
+
# python interpreter (>= 2.3)
PYTHON=python
@@ -13,22 +31,6 @@
# HTML tidy (needs not to be set if tidy usage is disabled, see below)
TIDY=tidy
-# dirs to copy to build target
-STATICDIRS=css img media misc
-
-# build target (attention: ~ will not work!)
-OUTPUTROOT=$(HOME)/isabelle/website_test
-
-# location of isabelle distribution packages
-ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
-
-# location of doc content file
-ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/Isabelle2005/doc/Contents
-
-# umask for target files
-TARGET_UMASK_FILE=664
-TARGET_UMASK_DIR=775
-
# set to a true value to use the "pypager iso-8859-1" hack
# (may be neccessary for older versions of HTML tidy)
FORCE_ISO_8859_1=
--- a/Admin/website/build/localconf.sun.template.mak Tue Oct 04 08:14:15 2005 +0200
+++ b/Admin/website/build/localconf.sun.template.mak Tue Oct 04 08:49:24 2005 +0200
@@ -1,6 +1,24 @@
# isaweb configuration
# $Id$
+# build target (attention: ~ will not work!)
+OUTPUTROOT=$(HOME)/isabelle/website_test
+#~ OUTPUTROOT=/home/proj/isabelle/website
+
+# location of isabelle distribution packages
+ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
+
+# location of doc content file
+ISABELLE_DOC_CONTENT_FILE=$(ISABELLE_DIST)/Isabelle2005/doc/Contents
+
+# dirs to copy to build target
+STATICDIRS=css img media misc
+
+# umask/group for target files
+TARGET_UMASK_FILE=664
+TARGET_UMASK_DIR=775
+TARGET_GROUP=isabelle
+
# python interpreter (>= 2.3)
PYTHON=python2.3
@@ -13,22 +31,6 @@
# HTML tidy (needs not to be set if tidy usage is disabled, see below)
TIDY=tidy
-# dirs to copy to build target
-STATICDIRS=css img media misc
-
-# build target (attention: ~ will not work!)
-OUTPUTROOT=$(HOME)/isabelle/website_test
-
-# location of isabelle distribution packages
-ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
-
-# location of doc content file
-ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/Isabelle2005/doc/Contents
-
-# umask for target files
-TARGET_UMASK_FILE=664
-TARGET_UMASK_DIR=775
-
# set to a true value to use the "pypager iso-8859-1" hack
# (may be neccessary for older versions of HTML tidy)
FORCE_ISO_8859_1=
--- a/Admin/website/build/main.mak Tue Oct 04 08:14:15 2005 +0200
+++ b/Admin/website/build/main.mak Tue Oct 04 08:49:24 2005 +0200
@@ -74,48 +74,7 @@
# build dependencies
$(DEP_FILE): $(CONF)
- rm -f $(DEP_FILE); \
- touch $(DEP_FILE); \
- echo '# This is a generated file; do not edit' >> $(DEP_FILE); \
- echo >> $(DEP_FILE); \
- allstatic=''; \
- for dir in $(STATICDIRS); \
- do \
- for file in `$(FIND) $$dir -follow -type f -a ! -path "*/CVS/*"`; \
- do \
- outputfile=$(OUTPUTROOT)/$$file; \
- outputdir=`dirname $$outputfile`; \
- echo "$$outputfile: $$file" >> $(DEP_FILE); \
- echo " mkdir -p $$outputdir" >> $(DEP_FILE); \
- echo " -chmod $(TARGET_UMASK_DIR) $$outputdir" >> $(DEP_FILE); \
- echo ' cp $$< $$@' >> $(DEP_FILE); \
- echo ' chmod $(TARGET_UMASK_FILE) $$@' >> $(DEP_FILE); \
- allstatic="$$allstatic$$outputfile "; \
- echo >> $(DEP_FILE); \
- done; \
- done; \
- echo "DEP_ALLSTATIC=$$allstatic" >> $(DEP_FILE); \
- echo >> $(DEP_FILE); \
- echo 'DEP_HTML=$$(DEP_ALLSTATIC) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
- echo >> $(DEP_FILE); \
- allhtml=''; \
- for html in `$(FIND) . -name "*.html" -a ! -name "*.include.html"`; \
- do \
- outputfile=$(OUTPUTROOT)/$$html; \
- outputdir=`dirname $$outputfile`; \
- echo "$$outputfile: $$html"' $$(DEP_HTML)' >> $(DEP_FILE); \
- echo " mkdir -p $$outputdir" >> $(DEP_FILE); \
- echo " -chmod $(TARGET_UMASK_DIR) $$outputdir" >> $(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_FILE) $$@' >> $(DEP_FILE); \
- allhtml="$$allhtml$$outputfile "; \
- echo >> $(DEP_FILE); \
- done; \
- echo "DEP_ALLHTML=$$allhtml" >> $(DEP_FILE); \
- echo >> $(DEP_FILE); \
- echo 'allsite: $$(DEP_ALLHTML) $$(DEP_ALLSTATIC)' >> $(DEP_FILE); \
- echo ".PHONY: allsite" >> $(DEP_FILE)
+ build/make_dep.bash "$(FIND)" "$(OUTPUTROOT)" "$(DEP_FILE)" "$(STATICDIRS)"
# build dependencies explicitly
depends:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/build/make_dep.bash Tue Oct 04 08:49:24 2005 +0200
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# $Id$
+
+# build make dependency file
+
+# parameters
+FIND="$1"
+OUTPUTROOT="$2"
+DEP_FILE="$3"
+STATICDIRS="$4"
+
+rm -f "$DEP_FILE"
+touch "$DEP_FILE"
+echo '# This is a generated file; do not edit' >> "$DEP_FILE"
+echo >> "$DEP_FILE"
+allstatic=''
+for dir in $STATICDIRS
+do
+ for file in $("$FIND" "$dir" -follow -type f -a ! -path "*/CVS/*")
+ do
+ outputfile="\$(OUTPUTROOT)/$file"
+ echo "$outputfile: $file" >> "$DEP_FILE"
+ echo ' mkdir -p $(dir $@)' >> "$DEP_FILE"
+ echo ' -chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE"
+ echo ' -chgrp $(TARGET_GROUP) $(dir $@)' >> "$DEP_FILE"
+ echo ' cp $< $@' >> "$DEP_FILE"
+ echo ' chmod $(TARGET_UMASK_DIR) $@' >> "$DEP_FILE"
+ echo ' chgrp $(TARGET_GROUP) $@' >> "$DEP_FILE"
+ allstatic="$allstatic$outputfile "
+ echo >> "$DEP_FILE"
+ done
+done
+echo "DEP_ALLSTATIC=$allstatic" >> "$DEP_FILE"
+echo >> "$DEP_FILE"
+echo 'DEP_HTML=$(DEP_ALLSTATIC) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> "$DEP_FILE"
+echo >> "$DEP_FILE"
+allhtml=''
+for html in $("$FIND" . -name "*.html" -a ! -name "*.include.html")
+do
+ outputfile="\$(OUTPUTROOT)/$html"
+ echo "$outputfile: $html \$(DEP_HTML)" >> "$DEP_FILE"
+ echo ' mkdir -p $(dir $@)' >> "$DEP_FILE"
+ echo ' -chmod $(TARGET_UMASK_DIR) $(dir $@)' >> "$DEP_FILE"
+ echo ' -chgrp $(TARGET_GROUP) $(dir $@)' >> "$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"
+ echo ' chgrp $(TARGET_GROUP) $@' >> "$DEP_FILE"
+ allhtml="$allhtml$outputfile "; \
+ echo >> "$DEP_FILE"
+done; \
+echo "DEP_ALLHTML=$allhtml" >> "$DEP_FILE"
+echo >> "$DEP_FILE"
+echo 'allsite: $(DEP_ALLHTML) $(DEP_ALLSTATIC)' >> "$DEP_FILE"
+echo ".PHONY: allsite" >> "$DEP_FILE"