|
|
1.1 ! root 1: #!/bin/sh ! 2: # Auxiliary script to work around TeX 3.0 bug. ! 3: # patches texinfo.tex in current directory, or in directory given as arg. ! 4: ! 5: ANYVERSION=no ! 6: ! 7: for arg in $1 $2 ! 8: do ! 9: case $arg in ! 10: --dammit | -d ) ANYVERSION=yes ;; ! 11: ! 12: * ) dir=$arg ! 13: esac ! 14: done ! 15: ! 16: if [ -z "$dir" ]; then ! 17: dir='.' ! 18: fi ! 19: ! 20: if [ \( 2 -lt $# \) -o \ ! 21: \( ! -f $dir/texinfo.tex \) ]; then ! 22: echo "To patch texinfo.tex for peaceful coexistence with Unix TeX 3.0," ! 23: echo "run $0" ! 24: echo "with no arguments in the same directory as texinfo.tex; or run" ! 25: echo " $0 DIRECTORY" ! 26: echo "(where DIRECTORY is a path leading to texinfo.tex)." ! 27: exit ! 28: fi ! 29: ! 30: if [ -z "$TMPDIR" ]; then ! 31: TMPDIR=/tmp ! 32: fi ! 33: ! 34: echo "Checking for \`dummy.tfm'" ! 35: ! 36: ( cd $TMPDIR; tex '\relax \batchmode \font\foo=dummy \bye' ) ! 37: ! 38: grep -s '3.0' $TMPDIR/texput.log ! 39: if [ 1 = "$?" -a "$ANYVERSION" != "yes" ]; then ! 40: echo "You probably do not need this patch," ! 41: echo "since your TeX does not seem to be version 3.0." ! 42: echo "If you insist on applying the patch, run $0" ! 43: echo "again with the option \`--dammit'" ! 44: exit ! 45: fi ! 46: ! 47: grep -s 'file not found' $TMPDIR/texput.log ! 48: if [ 0 = $? ]; then ! 49: echo "This patch requires the dummy font metric file \`dummy.tfm'," ! 50: echo "which does not seem to be part of your TeX installation." ! 51: echo "Please get your TeX maintainer to install \`dummy.tfm'," ! 52: echo "then run this script again." ! 53: exit ! 54: fi ! 55: rm $TMPDIR/texput.log ! 56: ! 57: echo "Patching $dir/texinfo.tex" ! 58: ! 59: sed -e 's/%%*\\font\\nullfont/\\font\\nullfont/' \ ! 60: $dir/texinfo.tex >$TMPDIR/texinfo.tex ! 61: mv $dir/texinfo.tex $dir/texinfo.tex-distrib; mv $TMPDIR/texinfo.tex $dir ! 62: ! 63: if [ 0 = $? ]; then ! 64: echo "Patched $dir/texinfo.tex to avoid TeX 3.0 bug." ! 65: echo "The original version is saved as $dir/texinfo.tex-distrib." ! 66: else ! 67: echo "Patch failed. Sorry." ! 68: fi
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.