loops/etc/make_docus

26 lines
570 B
Plaintext
Raw Permalink Normal View History

2017-10-16 19:43:09 +00:00
#! /bin/bash
cd /opt/gap4r5/local/pkg/loops/doc
rm -f manual.aux manual.dvi \
manual.idx manual.ilg \
manual.ind manual.lab \
manual.log manual.pdf \
manual.ps manual.six \
manual.toc
echo "*** Producing DVI files ***"
tex manual &> /dev/null
tex manual &> /dev/null
/usr/local/lib/gap4r4/doc/manualindex manual &> /dev/null
tex manual &> /dev/null
echo "*** Producing PDF & PS files ***"
pdftex manual &> /dev/null
dvips manual &> /dev/null
echo "*** Producing HTML files ***"
rm ../htm/*
../etc/convert.pl -icu -n loops ./ ../htm/