diff options
| -rwxr-xr-x | Master/texmf/scripts/texlive/texdoc.tlu | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Master/texmf/scripts/texlive/texdoc.tlu b/Master/texmf/scripts/texlive/texdoc.tlu index 5b88a678734..d106d533a61 100755 --- a/Master/texmf/scripts/texlive/texdoc.tlu +++ b/Master/texmf/scripts/texlive/texdoc.tlu @@ -398,11 +398,17 @@ else -- since we don't support msdos, if os.type is not windows, it's unix end end --- now a particular case for config.ext_list +-- now a particular case for config.ext_list and zip-relted stuff if support_zipped then set_config_element('ext_list', '.pdf, .pdf.gz, .pdf.bz2, .dvi, .dvi.gz, .dvi.bz2,'.. '.ps, .ps.gz, .ps.bz2, .txt, .txt.gz, .txt.bz2, .html') + set_config_list { + unzip_gz = 'gzip -d -c ', + unzip_bz2 = 'bzip -d -c ', + rm_file = 'rm -f', + rm_dir = 'rmdir' + } else set_config_element('ext_list', '.pdf, .html, .txt, .dvi, .ps') end |