Admin/page/Makefile
changeset 8133 ba1498046ee6
parent 8132 b93992e26c6a
child 9920 9734f2717203
equal deleted inserted replaced
8132:b93992e26c6a 8133:ba1498046ee6
     1 # --- uses $DISTNAME environment variable 
     1 # --- uses $DISTNAME environment variable 
       
     2 
       
     3 # -- makefile for Isabelle web pages (dist and main)
       
     4 # -- $Id$
     2 
     5 
     3 # --- perl scripts used in this makefile
     6 # --- perl scripts used in this makefile
     4 
     7 
     5 GENPAGE   = bin/genpage
     8 GENPAGE   = bin/genpage
     6 MKCONTENT = bin/mkcontents
     9 MKCONTENT = bin/mkcontents