make_doc

#!/bin/sh -e

echo "TeXing documentation"

# TeX the manual
tex manual; tex manual

# build the index
../../../doc/manualindex manual

# TeX the manual again to get cross-references right
tex manual; tex manual

# create PDF version
pdftex manual; pdftex manual

# create HTML version
mkdir -p ../htm
echo "Creating HTML documentation"
../../../etc/convert.pl -i -t -c -n FPLSA . ../htm