doc-src/Makefile.in
author wenzelm
Wed, 05 May 1999 18:16:03 +0200
changeset 6596 d44dd0b564c4
parent 6593 62204772812f
child 6604 d646567156c3
permissions -rw-r--r--
tuned;
     1 #
     2 # $Id$
     3 #
     4 # Common part for Doc Makefiles
     5 #
     6 
     7 ## settings
     8 
     9 LATEX = latex
    10 BIBTEX = bibtex
    11 RAIL = rail
    12 SEDINDEX = ../sedindex
    13 
    14 GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.blg
    15 OUTPUT = *.dvi *.pdf *.ps
    16 
    17 
    18 ## actions
    19 
    20 nothing:
    21 
    22 clean:
    23 	@rm -f $(GARBAGE)
    24 
    25 veryclean:
    26 	@rm -f $(OUTPUT) $(GARBAGE)
    27 
    28 isabelle.eps:
    29 	test -r $* || ln -s ../gfx/$* .
    30 
    31 isabelle_hol.eps:
    32 	test -r $* || ln -s ../gfx/$* .
    33 
    34 isabelle_zf.eps:
    35 	test -r $* || ln -s ../gfx/$* .