Admin/page/Makefile
changeset 15933 7f3ccb84e60d
parent 15886 c5d873a86e0f
equal deleted inserted replaced
15932:2c351ab6c403 15933:7f3ccb84e60d
     1 # -- makefile for Isabelle web pages (dist and main)
     1 # -- makefile for Isabelle web pages (dist and main)
     2 # -- $Id$
     2 # -- $Id$
       
     3 
       
     4 # --- force shell
       
     5 SHELL=bash
       
     6 
       
     7 # --- check parameters
       
     8 ifeq ($(tidy),)
       
     9     TIDYCMD=:
       
    10 else
       
    11     TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \
       
    12                 --logical-emphasis yes --gnu-emacs yes --write-back yes
       
    13 endif
     3 
    14 
     4 # --- external tools
    15 # --- external tools
     5 
    16 
     6 GENPAGE   = ./bin/genpage
    17 GENPAGE   = ./bin/genpage
     7 MKCONTENT = ./bin/mkcontents
    18 MKCONTENT = ./bin/mkcontents
    46 
    57 
    47 main:
    58 main:
    48 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
    59 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
    49 	@env DISTNAME=`cat DISTNAME` \
    60 	@env DISTNAME=`cat DISTNAME` \
    50 	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
    61 	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
       
    62 	-@cd $(MAIN_TARGET); \
       
    63         for html in *.html; \
       
    64             do $(TIDYCMD) $$html; \
       
    65         done
    51 
    66 
    52 pub-main: main
    67 pub-main: main
    53 	@echo "Publishing main pages (*.html only)."
    68 	@echo "Publishing main pages (*.html only)."
    54 	scp main/*.html $(MAIN_PUB_MIRROR_SRC)
    69 	scp main/*.html $(MAIN_PUB_MIRROR_SRC)
    55 	scp main/*.html $(MAIN_PUB_DEST)
    70 	scp main/*.html $(MAIN_PUB_DEST)
    56 
    71 
    57 dist:
    72 dist:
    58 	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    73 	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    59 	@env DISTNAME=`cat DISTNAME` \
    74 	@env DISTNAME=`cat DISTNAME` \
    60 	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
    75 	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
       
    76 	-@cd $(MAIN_TARGET); \
       
    77         for html in *.html; \
       
    78             do $(TIDYCMD) $$html; \
       
    79         done
    61 
    80 
    62 pub-dist: dist
    81 pub-dist: dist
    63 	@echo "Publishing dist pages (*.html only)."
    82 	@echo "Publishing dist pages (*.html only)."
    64 	scp dist/*.html $(DIST_PUB_DEST)
    83 	scp dist/*.html $(DIST_PUB_DEST)
    65 
    84