diff options
Diffstat (limited to 'editor')
| -rw-r--r-- | editor/editor_builders.py | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/editor/editor_builders.py b/editor/editor_builders.py index ff0daa86ff..67d4b8534f 100644 --- a/editor/editor_builders.py +++ b/editor/editor_builders.py @@ -26,7 +26,9 @@ def make_doc_header(target, source, env): decomp_size = len(buf) import zlib - buf = zlib.compress(buf) + # Use maximum zlib compression level to further reduce file size + # (at the cost of initial build times). + buf = zlib.compress(buf, zlib.Z_BEST_COMPRESSION) g.write("/* THIS FILE IS GENERATED DO NOT EDIT */\n") g.write("#ifndef _DOC_DATA_RAW_H\n") @@ -92,7 +94,9 @@ def make_translations_header(target, source, env, category): with open(sorted_paths[i], "rb") as f: buf = f.read() decomp_size = len(buf) - buf = zlib.compress(buf) + # Use maximum zlib compression level to further reduce file size + # (at the cost of initial build times). + buf = zlib.compress(buf, zlib.Z_BEST_COMPRESSION) name = os.path.splitext(os.path.basename(sorted_paths[i]))[0] g.write("static const unsigned char _{}_translation_{}_compressed[] = {{\n".format(category, name)) |