make "CC=gcc" TeX
if [ ! -f $TEXDIR/virtex ]
then
echo "*** ISITEX: make failed. Stop." 1>&2
exit 2
fi
( cd $TEXDIR; mv tex.pool isitex.pool )
make formats
if [ ! -f $TEXSRC/stamp-formats ]
then
echo "*** ISITEX: make formats failed. Stop." 1>&2
exit 2
fi
echo
echo "ISITEX has been successfully compiled, and the format files have been"
echo "generated. Now follow the guidelines from the README file for further"
echo "installation. Do not forget to copy $TEXDIR/isitex.pool"
echo "to your TEXPOOL-Directory."
echo