diff options
author | Karl Berry <karl@freefriends.org> | 2023-03-27 21:26:26 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2023-03-27 21:26:26 +0000 |
commit | e55e229e13434f5752b115d04b65f0f79a8c53b5 (patch) | |
tree | df67233797eced90f1d8fac37def6772edb028e3 /Master/texmf-dist/source/generic/tex4ht/update-htfonts | |
parent | 92db61824f7f439f7668c877881b0472130f035a (diff) |
disable accent redefinition, tex4ht r1311; do not redefine \chapter, tex4ht r1312
git-svn-id: svn://tug.org/texlive/trunk@66688 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/source/generic/tex4ht/update-htfonts')
-rw-r--r-- | Master/texmf-dist/source/generic/tex4ht/update-htfonts | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/Master/texmf-dist/source/generic/tex4ht/update-htfonts b/Master/texmf-dist/source/generic/tex4ht/update-htfonts index 1b24cc5ec45..e07d1e0b075 100644 --- a/Master/texmf-dist/source/generic/tex4ht/update-htfonts +++ b/Master/texmf-dist/source/generic/tex4ht/update-htfonts @@ -1,5 +1,6 @@ #!/bin/sh # $Id: update-htfonts 1141 2022-06-01 21:43:42Z karl $ +# Update TeX4ht font files (.htf). See ./Makefile for invocations. # Public domain. Originally written by Karl Berry, 2022. # don't bother with real option parsing. @@ -34,7 +35,8 @@ fi devdir=$1 instdir=$2 verbose=true -tmp=/tmp/htdif # prefix +tmpdir=/tmp/htdif.d # prefix +rm -rf $tmpdir; mkdir $tmpdir if test ! -d "$devdir"; then echo "$0: devdir not a directory: $devdir" >&2 @@ -66,8 +68,8 @@ copy_file () { htf_same () { src=$1; dest=$2; # - src_filtered=$tmp.s`basename "$src"` - dest_filtered=$tmp.d`basename "$dest"` + src_filtered=$tmpdir/s`basename "$src"` + dest_filtered=$tmpdir/d`basename "$dest"` # sed 's/20[0-9][0-9]-[0-9][0-9]-[0-9][0-9]\(-[0-9][0-9]:[0-9][0-9]\)*//' \ $src >$src_filtered || exit 1 @@ -79,7 +81,7 @@ htf_same () { # Iterate through all files in the dev directory. echo "$prg: comparing $devdir" echo "$prg: to $instdir" ->$tmp.0 # accumulate diffs here +>$tmpdir/0 # accumulate diffs here # find "$devdir" -type f -print | sort | while read devf; do instf=`echo "$devf" | sed "s,^$devdir/,$instdir/,"` @@ -93,7 +95,7 @@ find "$devdir" -type f -print | sort | while read devf; do else $verbose && echo "`basename \"$devf\"`: diff ($devf != $instf)" # save diff from (older) DEST to newer (SRC). - diff -u0 "$dest" "$src" >>$tmp.0 + diff -u0 "$dest" "$src" >>$tmpdir/0 # copy_file "$devf" "$instf" fi @@ -122,14 +124,14 @@ find "$devdir" -type f -print | sort | while read devf; do done # check for extra files in $instdir -(cd "$devdir" && find . -type f -print | sort) >$tmp.devdir || exit 1 -(cd "$instdir" && find . -type f -print | sort) >$tmp.instdir || exit 1 +(cd "$devdir" && find . -type f -print | sort) >$tmpdir/devdir || exit 1 +(cd "$instdir" && find . -type f -print | sort) >$tmpdir/instdir || exit 1 echo "$prg: files in devdir and not in instdir (should be empty):" -comm -23 $tmp.devdir $tmp.instdir +comm -23 $tmpdir/devdir $tmpdir/instdir echo "$prg: files in instdir and not in devdir (you should remove):" -comm -13 $tmp.devdir $tmp.instdir +comm -13 $tmpdir/devdir $tmpdir/instdir # maybe better to leave it for manual removal? echo "$prg: done." |