Admin/page/Makefile
changeset 15810 2c119fed01f0
parent 14582 f0779f6fa7e8
child 15886 c5d873a86e0f
equal deleted inserted replaced
15809:3355abbeced1 15810:2c119fed01f0
    32 
    32 
    33 # --- target include files with documentation links
    33 # --- target include files with documentation links
    34 DOC_CONTENTS_MAIN = docu-contents.main
    34 DOC_CONTENTS_MAIN = docu-contents.main
    35 DOC_CONTENTS_DIST = docu-contents.dist
    35 DOC_CONTENTS_DIST = docu-contents.dist
    36 
    36 
       
    37 # --- target directories for publishing to web site
       
    38 MAIN_PUB_MIRROR_SRC=sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle-repository/www/
       
    39 MAIN_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/
       
    40 DIST_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/
       
    41 
    37 # ---
    42 # ---
    38 # --- begin rules
    43 # --- begin rules
    39 
    44 
    40 all: clean main dist install weblint
    45 all: clean main dist install weblint
    41 
    46 
    42 main:
    47 main:
    43 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
    48 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
    44 	@env DISTNAME=`cat DISTNAME` \
    49 	@env DISTNAME=`cat DISTNAME` \
    45 	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
    50 	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
    46 
    51 
       
    52 pub-main: main
       
    53 	@echo "Publishing main pages."
       
    54 	scp main/* $(MAIN_PUB_MIRROR_SRC)
       
    55 	scp main/* $(MAIN_PUB_DEST)
       
    56 
    47 dist:
    57 dist:
    48 	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    58 	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    49 	@env DISTNAME=`cat DISTNAME` \
    59 	@env DISTNAME=`cat DISTNAME` \
    50 	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
    60 	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
       
    61 
       
    62 pub-dist: dist
       
    63 	@echo "Publishing dist pages."
       
    64 	scp dist/*.html $(DIST_PUB_DEST)
    51 
    65 
    52 install: main dist
    66 install: main dist
    53 	@cp -R dist/. ..
    67 	@cp -R dist/. ..
    54 	@mkdir -p ../../main-`cat DISTNAME`/.
    68 	@mkdir -p ../../main-`cat DISTNAME`/.
    55 	@cp -R main/. ../../main-`cat DISTNAME`/.
    69 	@cp -R main/. ../../main-`cat DISTNAME`/.