doc-src/Makefile.in
author wenzelm
Wed, 05 May 1999 18:07:38 +0200
changeset 6593 62204772812f
child 6596 d44dd0b564c4
permissions -rw-r--r--
Common part for Doc Makefiles;
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
62204772812f Common part for Doc Makefiles;
wenzelm
parents:
diff changeset
    14
GARBAGE = *.aux *.log *.toc *.idx *.rai *.bbl *.ind *.blg
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
62204772812f Common part for Doc Makefiles;
wenzelm
parents:
diff changeset
    25
veryclean:
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/$* .