max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(bin/linja): support files with spaces

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-16 09:18:10 -04:00 • committed by Leonardo de Moura
parent 067484a3e5
commit a7fe8cf15c
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

@ -463,7 +463,7 @@ def make_build_ninja(args):
print("""rule LEAN""", file=f)
print(""" depfile = ${DLEAN_FILE}""", file=f)
print(""" command = "%s" %s -o ${OLEAN_FILE} $in""" \
print(""" command = "%s" %s -o "${OLEAN_FILE}" $in""" \
% (g_lean_path, " ".join(args.lean_options)), file=f)
print("build all: phony", end=' ', file=f)