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