From 340ba7780e012b45b4c5ce3be6077495f3591db5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 14 Jan 2017 18:57:10 +0000 Subject: [PATCH] Added MAKEJOBS env var to mk_unix_dist.py --- scripts/mk_unix_dist.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 527797e66..488bc4364 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -27,6 +27,7 @@ DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False PYTHON_ENABLED=True +MAKEJOBS=getenv("MAKEJOBS", '8') def set_verbose(flag): global VERBOSE @@ -139,7 +140,7 @@ class cd: def mk_z3(): with cd(BUILD_DIR): try: - return subprocess.call(['make', '-j', '8']) + return subprocess.call(['make', '-j', MAKEJOBS]) except: return 1