diff options
Diffstat (limited to 'Master/texmf-dist/source/generic/tex4ht/update-htfonts')
-rw-r--r-- | Master/texmf-dist/source/generic/tex4ht/update-htfonts | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/generic/tex4ht/update-htfonts b/Master/texmf-dist/source/generic/tex4ht/update-htfonts index 7791efcf3a0..b30e3e7a915 100644 --- a/Master/texmf-dist/source/generic/tex4ht/update-htfonts +++ b/Master/texmf-dist/source/generic/tex4ht/update-htfonts @@ -134,4 +134,16 @@ echo "$prg: files in instdir and not in devdir (you should remove):" comm -13 $tmpdir/devdir $tmpdir/instdir # maybe better to leave it for manual removal? +# also copy source files. +t4srcdir=`echo "$instdir" \ + | sed 's,/texmf-dist/.*,/texmf-dist/source/generic/tex4ht,'` +echo "$prg: copying source files to $t4srcdir." +cp -p ChangeLog Makefile tex4ht-fonts*.tex update-htfonts "$t4srcdir" + +echo +(set -x; + $svn status "$instdir" + $svn status "$t4srcdir" +) + echo "$prg: done." |