doc-src/Main/Makefile
author nipkow
Wed, 11 Mar 2009 12:51:00 +0100
changeset 30442 1bc0638d554d
child 30457 28b487cd9e15
permissions -rw-r--r--
Added "What's in Main" to doc sources

#
# $Id$
#

## targets

default: dvi


## dependencies

include ../Makefile.in

SRC = ../../src/HOL/Docs/generated

NAME = main

FILES = $(NAME).tex Main_Doc.tex \
  isabelle.sty isabellesym.sty pdfsetup.sty

dvi: $(NAME).dvi

$(NAME).dvi: $(FILES)
	$(LATEX) $(NAME)

pdf: $(NAME).pdf

$(NAME).pdf: $(FILES)
	$(PDFLATEX) $(NAME)
	$(FIXBOOKMARKS) $(NAME).out
	$(PDFLATEX) $(NAME)
	$(PDFLATEX) $(NAME)

isabelle.sty:
	ln ../isabelle.sty .

isabellesym.sty:
	ln ../isabellesym.sty .

pdfsetup.sty:
	ln ../pdfsetup.sty .

copy:
	cp $(SRC)/Main_Doc.tex Main_Doc.tex
	cp $(SRC)/root.tex main.tex