doc-src/System/Makefile
author wenzelm
Wed May 05 18:41:31 1999 +0200 (1999-05-05)
changeset 6601 51eed1aefccd
parent 6600 5a94bd71cc41
child 6623 021728c71030
permissions -rw-r--r--
fixed FILES;
     1 #
     2 # $Id$
     3 #
     4 
     5 ## targets
     6 
     7 default: dvi
     8 dist: dvi
     9 
    10 
    11 ## dependencies
    12 
    13 include ../Makefile.in
    14 
    15 NAME = system
    16 FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
    17 	../iman.sty ../extra.sty
    18 
    19 dvi: $(NAME).dvi
    20 
    21 $(NAME).dvi: $(FILES) isabelle.eps
    22 	touch $(NAME).ind
    23 	$(LATEX) $(NAME)
    24 	$(LATEX) $(NAME)
    25 	$(SEDINDEX) $(NAME)
    26 	$(LATEX) $(NAME)