diff options
| author | Jussi Pakkanen <jpakkane@gmail.com> | 2013-02-10 21:12:15 +0200 |
|---|---|---|
| committer | Jussi Pakkanen <jpakkane@gmail.com> | 2013-02-10 21:12:15 +0200 |
| commit | 75dbc2abdb4103a59a7b348b29fc5b48da7e9012 (patch) | |
| tree | 0af8bfb98405fbe8ce86797015bdab813c6d0dcb /builder_install.py | |
| parent | 399c2104fe775932877adb261eb0f9c177ff6677 (diff) | |
| download | meson-75dbc2abdb4103a59a7b348b29fc5b48da7e9012.tar.gz | |
Compress man files.
Diffstat (limited to 'builder_install.py')
| -rwxr-xr-x | builder_install.py | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/builder_install.py b/builder_install.py index 67537dba9..9df56127d 100755 --- a/builder_install.py +++ b/builder_install.py @@ -50,7 +50,10 @@ def install_man(d): outdir = os.path.split(outfilename)[0] os.makedirs(outdir, exist_ok=True) print('Installing %s to %s.' % (fullfilename, outdir)) - shutil.copyfile(fullfilename, outfilename) + if outfilename.endswith('.gz') and not fullfilename.endswith('.gz'): + open(outfilename, 'wb').write(gzip.compress(open(fullfilename, 'rb').read())) + else: + shutil.copyfile(fullfilename, outfilename) shutil.copystat(fullfilename, outfilename) def install_headers(d): |