1# =====================================================================
2# Makefile for the unwind library documentation 
3# =====================================================================
4
5# ---------------------------------------------------------------------
6# Pathname to the unwind help files
7# ---------------------------------------------------------------------
8Help=../help
9
10# ---------------------------------------------------------------------
11# Pathname to the doc-to-tex script and doc-to-tex.sed file 
12# ---------------------------------------------------------------------
13DOCTOTEX=../../../Manual/Reference/bin/doc-to-tex
14DOCTOTEXSED=../../../Manual/Reference/bin/doc-to-tex.sed
15DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
16
17# ---------------------------------------------------------------------
18# Pathname to the makeindex script
19# ---------------------------------------------------------------------
20MAKEINDEX=makeindex
21
22default:
23	@echo "INSTRUCTIONS: Type \"make all\" to make the documentation"
24
25# ---------------------------------------------------------------------
26# Remove all trace of previous LaTeX jobs
27# ---------------------------------------------------------------------
28clean:
29	rm -f *.dvi *.aux *.toc *.log *.idx *.ilg *.ind \
30		entries.tex index.tex \
31		unwind.ps unwind.pdf
32
33tex: ids
34	@echo "\begin{theindex}" > index.tex
35	@echo "\mbox{}" >> index.tex
36	@echo "\end{theindex}" >> index.tex
37	@echo "TeX files made"
38
39ids:
40	@echo "\chapter{ML Functions in the unwind Library}">entries.tex
41	@echo "\input{entries-intro}" >> entries.tex
42	${DOCTOTEXEXE} ${Help}/entries entries.tex
43
44index: 
45	${MAKEINDEX} unwind.idx index.tex
46
47unwind: 
48	latex unwind.tex
49
50ps:
51	dvips unwind.dvi -o
52
53pdf:	unwind.ps
54	pdflatex unwind.tex
55
56all: 
57	make clean; make tex; make unwind; make index; make unwind ps pdf
58