doc-src/Makefile.in
author wenzelm
Wed, 05 May 1999 18:35:41 +0200
changeset 6600 5a94bd71cc41
parent 6596 d44dd0b564c4
child 6604 d646567156c3
permissions -rw-r--r--
improved Makefile;

#
# $Id$
#
# Common part for Doc Makefiles
#

## settings

LATEX = latex
BIBTEX = bibtex
RAIL = rail
SEDINDEX = ../sedindex

GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.blg
OUTPUT = *.dvi *.pdf *.ps


## actions

nothing:

clean:
	@rm -f $(GARBAGE)

veryclean:
	@rm -f $(OUTPUT) $(GARBAGE)

isabelle.eps:
	test -r $* || ln -s ../gfx/$* .

isabelle_hol.eps:
	test -r $* || ln -s ../gfx/$* .

isabelle_zf.eps:
	test -r $* || ln -s ../gfx/$* .