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

fix(bin/lmake): fix typo LEAN_OPTIONS

Browse source
This commit is contained in:
Soonho Kong 2014-08-06 20:51:26 -07:00
parent 8d4c7b4b2c
commit 9b23a52d0f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
bin/lmake
View file

@ -89,8 +89,8 @@ def find_lean_exe():
return False
def find_lean_opt():
""" Return a list of lean options from env_var LEAN_OPTION"""
lean_opt = os.environ.get('LEAN_OPTION')
""" Return a list of lean options from env_var LEAN_OPTIONS """
lean_opt = os.environ.get('LEAN_OPTIONS')
return string.split(lean_opt) if lean_opt is not None else []
def call_lean(leanfile, options):