michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(bin/lmake): pass lmake option to makefile

Browse source
This commit is contained in:
Soonho Kong 2014-08-07 08:03:23 -07:00
parent f523c25c52
commit f209ae5725
1 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
bin/lmake
View file

@ -137,10 +137,15 @@ def get_target(s):
oleanfile = get_olean(s)
return oleanfile if oleanfile is not None else s
def call_makefile(directory, makefile, args):
def call_makefile(directory, makefile, args, lean_options):
""" Call makefile with a target generated from a given arg """
env_copy = os.environ.copy()
env_copy['LEAN'] = find_lean_exe()
lean_options_str = ' '.join(lean_options)
if env_copy.get("LEAN_OPTIONS"):
env_copy['LEAN_OPTIONS'] = env_copy['LEAN_OPTIONS'] + lean_options_str
else:
env_copy['LEAN_OPTIONS'] = lean_options_str
cmd = ["make", "-j"]
if makefile:
cmd = cmd + ["--makefile", makefile]
@ -178,11 +183,12 @@ def main(argv=None):
if makefile:
directory = os.path.dirname(makefile)
if directory or makefile:
call_makefile(directory, makefile, args)
for arg in args:
leanfile = get_lean(arg)
if leanfile is not None and os.path.isfile(leanfile):
call_lean(leanfile, lean_options)
call_makefile(directory, makefile, args, lean_options)
else:
for arg in args:
leanfile = get_lean(arg)
if leanfile and os.path.isfile(leanfile):
call_lean(leanfile, lean_options)
if __name__ == "__main__":
sys.exit(main())