1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
# Makefile for HOL Manual title and end pages. This is separate from the main
# manual stuff because of the heavy PostScript hacking involved.
# The following variables are needed:
#
# LATEX -- The name of the LaTeX command normally used at this site.
# DVI2PS -- The name of the dvi -> ps converter.
# DVI2PSOPTS -- Options for the converter named in DVI2PS.
LATEX = latex
DVI2PS = dvips
DVI2PSOPTS =
RM = rm -f
default:
@echo "$(DIR)"
@echo "INSTRUCTIONS: Type \"make all\" to make the fancy covers."
@echo -n " NB - psfig macros required. See Covers/psfig/"
@echo " if you don't have them."
endpages.dvi: CRC.ps DESCRIPTION.ps LANTERN.ps REFERENCE.ps TUTORIAL.ps \
arms.ps endpages.tex endpages.sty
TEXINPUTS=$$(pwd)/psfig:$$TEXINPUTS $(LATEX) endpages
@echo "===> endpages.dvi created"
titlepages.dvi: CRC.ps DESCRIPTION.ps LANTERN.ps REFERENCE.ps TUTORIAL.ps \
arms.ps titlepages.tex titlepages.sty
TEXINPUTS=$$(pwd)/psfig:$$TEXINPUTS $(LATEX) titlepages
@echo "===> titlepages.dvi created"
dvi: endpages.dvi titlepages.dvi
endpages.ps: endpages.dvi
-$(DVI2PS) $(DVI2PSOPTS) endpages > endpages.ps
@echo "===> endpages.ps created"
titlepages.ps: titlepages.dvi
-$(DVI2PS) $(DVI2PSOPTS) titlepages > titlepages.ps
@echo "===> titlepages.ps created"
all: clobber endpages.ps titlepages.ps
clean:
$(RM) *.log core *.aux *~ #* LOG
@echo "===> Fancy end and title pages cleaned up"
clobber: clean
$(RM) endpages.ps titlepages.ps *.dvi
@echo "===> Fancy end and title pages clobbered"
|
