From 57410e781835dacd7e56c40e4c992bd0b22af9fc Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 4 Aug 2014 17:28:57 -0700 Subject: [PATCH] fix(bin/lmake): use '-j' option for make [skip ci] --- bin/lmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/lmake b/bin/lmake index 024edd4f2..9000eceaa 100755 --- a/bin/lmake +++ b/bin/lmake @@ -120,7 +120,7 @@ def call_makefile(makefile, arg): """ Call makefile with a target generated from a given arg """ env_copy = os.environ.copy() env_copy['LEAN'] = find_lean_exe() - cmd = ["make", "-C", os.path.dirname(makefile)] + cmd = ["make", "-j", "-C", os.path.dirname(makefile)] if arg: target = get_target(arg) cmd.append(target)