From 6f062a005e25463630bbe9998d8b6fbb338adc18 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 13 Aug 2014 21:04:56 -0700 Subject: [PATCH] fix(bin/lmake): remove debugging messages --- bin/lmake | 3 --- 1 file changed, 3 deletions(-) diff --git a/bin/lmake b/bin/lmake index 3bc67511e..edc6d8b3a 100755 --- a/bin/lmake +++ b/bin/lmake @@ -152,8 +152,6 @@ def call_makefile(directory, makefile, makefile_options, args, lean_options): if directory: cmd += ["-C", directory] cmd += makefile_options - print "LEAN_OPTIONS =", env_copy['LEAN_OPTIONS'] - print "CMD =", cmd for arg in args: target = get_target(arg) cmd.append(target) @@ -199,7 +197,6 @@ def extract_makefile_options(args): makefile_options.append("-j") elif args.jobs: makefile_options += ["-j", args.jobs] - print makefile_options return makefile_options def main(argv=None):