doc-src/Main/Makefile
author wenzelm
Wed, 11 Mar 2009 20:11:06 +0100
changeset 30457 28b487cd9e15
parent 30442 1bc0638d554d
child 42511 bf89455ccf9d
permissions -rw-r--r--
basic setup for "main" as generated Isabelle manual;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30442
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     1
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     2
## targets
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     3
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     4
default: dvi
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     5
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     6
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     7
## dependencies
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     8
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
     9
include ../Makefile.in
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    10
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    11
NAME = main
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    12
30457
28b487cd9e15 basic setup for "main" as generated Isabelle manual;
wenzelm
parents: 30442
diff changeset
    13
FILES = ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty $(NAME).tex	\
28b487cd9e15 basic setup for "main" as generated Isabelle manual;
wenzelm
parents: 30442
diff changeset
    14
  Docs/document/Main_Doc.tex
30442
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    15
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    16
dvi: $(NAME).dvi
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    17
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    18
$(NAME).dvi: $(FILES)
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    19
	$(LATEX) $(NAME)
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    20
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    21
pdf: $(NAME).pdf
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    22
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    23
$(NAME).pdf: $(FILES)
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents:
diff changeset
    24
	$(PDFLATEX) $(NAME)