loops/etc/make_docus
2017-10-16 21:43:09 +02:00

26 lines
570 B
Bash

#! /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/