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;
wenzelm@6600
     1
#
wenzelm@6600
     2
# $Id$
wenzelm@6600
     3
#
wenzelm@6600
     4
wenzelm@6600
     5
## targets
wenzelm@6600
     6
wenzelm@6600
     7
default: dvi
wenzelm@6600
     8
dist: dvi
wenzelm@3170
     9
wenzelm@3170
    10
wenzelm@6600
    11
## dependencies
wenzelm@6600
    12
wenzelm@6600
    13
include ../Makefile.in
wenzelm@6600
    14
wenzelm@6600
    15
NAME = system
wenzelm@6601
    16
FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
wenzelm@6601
    17
	../iman.sty ../extra.sty
wenzelm@3170
    18
wenzelm@6600
    19
dvi: $(NAME).dvi
wenzelm@3170
    20
wenzelm@6600
    21
$(NAME).dvi: $(FILES) isabelle.eps
wenzelm@6600
    22
	touch $(NAME).ind
wenzelm@6600
    23
	$(LATEX) $(NAME)
wenzelm@6600
    24
	$(LATEX) $(NAME)
wenzelm@6600
    25
	$(SEDINDEX) $(NAME)
wenzelm@6600
    26
	$(LATEX) $(NAME)