Common part for Doc Makefiles;
authorwenzelm
Wed, 05 May 1999 18:07:38 +0200
changeset 659362204772812f
parent 6592 c120262044b6
child 6594 fe2f5024f89e
Common part for Doc Makefiles;
doc-src/Makefile.in
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Makefile.in	Wed May 05 18:07:38 1999 +0200
     1.3 @@ -0,0 +1,35 @@
     1.4 +#
     1.5 +# $Id$
     1.6 +#
     1.7 +# Common part for Doc Makefiles
     1.8 +#
     1.9 +
    1.10 +## settings
    1.11 +
    1.12 +LATEX = latex
    1.13 +BIBTEX = bibtex
    1.14 +RAIL = rail
    1.15 +SEDINDEX = ../sedindex
    1.16 +
    1.17 +GARBAGE = *.aux *.log *.toc *.idx *.rai *.bbl *.ind *.blg
    1.18 +OUTPUT = *.dvi *.pdf *.ps
    1.19 +
    1.20 +
    1.21 +## actions
    1.22 +
    1.23 +nothing:
    1.24 +
    1.25 +clean:
    1.26 +	@rm -f $(GARBAGE)
    1.27 +
    1.28 +veryclean:
    1.29 +	@rm -f $(OUTPUT) $(GARBAGE)
    1.30 +
    1.31 +isabelle.eps:
    1.32 +	test -r $* || ln -s ../gfx/$* .
    1.33 +
    1.34 +isabelle_hol.eps:
    1.35 +	test -r $* || ln -s ../gfx/$* .
    1.36 +
    1.37 +isabelle_zf.eps:
    1.38 +	test -r $* || ln -s ../gfx/$* .