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