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

fix(bin/linja): bug that only happens when uisng linja on Windows

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-09 16:38:09 -08:00
parent c7ee831c69
commit daa9bb70b7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/linja.in
View file

@ -614,7 +614,7 @@ def build_olean(lean, olean, clean, dlean, ilean, base):
else: else:
str = """build %s %s: LEAN %s | %s""" % (olean, ilean, lean, dlean) str = """build %s %s: LEAN %s | %s""" % (olean, ilean, lean, dlean)
if g_lean_bin_dep_flag: if g_lean_bin_dep_flag:
str += " %s" % g_lean_path str += " %s" % normalize_drive_name(g_lean_path)
str += "\n" str += "\n"
str += " DLEAN_FILE=%s\n" % dlean str += " DLEAN_FILE=%s\n" % dlean
str += " OLEAN_FILE=%s\n" % olean str += " OLEAN_FILE=%s\n" % olean