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

fix(bin/linja): replace windows newline '\r\n' to unix newline '\n'

Browse source 
This should be handled by Python. However, when we use mingw-python
which acts like Unix Python with Native Windows Emacs, we have a problem
because mingw-python do not handle '\r'. This patch manually replace
'\r\n' with '\n' to solve the problem.

close #573
This commit is contained in:
Soonho Kong 2015-05-04 05:37:29 -04:00
parent 69f3f65ec9
commit 5e05a25a5d
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
bin/linja.in
View file

@ -515,9 +515,9 @@ def call_ninja(args):
proc = subprocess.Popen([g_ninja_path] + ninja_option + targets, stdout=proc_out, stderr=proc_err) proc = subprocess.Popen([g_ninja_path] + ninja_option + targets, stdout=proc_out, stderr=proc_err)
(out, err) = proc.communicate() (out, err) = proc.communicate()
if out is not None: if out is not None:
out = out.decode('utf-8') out = out.decode('utf-8').replace('\r\n', '\n')
if err is not None: if err is not None:
err = err.decode('utf-8') err = err.decode('utf-8').replace('\r\n', '\n')
if args.flycheck: if args.flycheck:
if len(args.targets) == 1 and (args.targets[0].endswith(".lean") or args.targets[0].endswith(".hlean")): if len(args.targets) == 1 and (args.targets[0].endswith(".lean") or args.targets[0].endswith(".hlean")):
process_lean_output(targets[0], out, args, args.targets[0].endswith(".hlean")) process_lean_output(targets[0], out, args, args.targets[0].endswith(".hlean"))
@ -530,7 +530,7 @@ def call_ninja(args):
def call_lean(filename, args): def call_lean(filename, args):
proc = subprocess.Popen([g_lean_path] + args.lean_options + [filename], proc = subprocess.Popen([g_lean_path] + args.lean_options + [filename],
stdout=subprocess.PIPE, stderr=subprocess.STDOUT) stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
out = proc.communicate()[0].decode('utf-8') out = proc.communicate()[0].decode('utf-8').replace('\r\n', '\n')
process_lean_output(filename, out, args, filename.endswith(".hlean")) process_lean_output(filename, out, args, filename.endswith(".hlean"))
return proc.returncode return proc.returncode
@ -685,8 +685,9 @@ def escape_dep(s):
def make_deps(lean_file, dlean_file, olean_file): def make_deps(lean_file, dlean_file, olean_file):
with open(dlean_file, "w") as f: with open(dlean_file, "w") as f:
deps = [] deps = []
proc = subprocess.Popen([g_lean_path, "--deps", lean_file], stdout=subprocess.PIPE, stderr=subprocess.STDOUT) proc = subprocess.Popen([g_lean_path, "--deps", lean_file],
output = proc.communicate()[0].decode('utf-8') stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
output = proc.communicate()[0].decode('utf-8').replace('\r\n', '\n')
print(escape_dep(olean_file) + ": \\", file=f) print(escape_dep(olean_file) + ": \\", file=f)
for olean_file in output.strip().splitlines(): for olean_file in output.strip().splitlines():
if olean_file: if olean_file: