From 72aadd1afae8ce278736d5632afe3c5d40b7f151 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Sun, 17 Aug 2014 17:30:43 -0700 Subject: [PATCH] fix(bin/lmake): save .olean file when makefile doesn't exist --- bin/lmake | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/bin/lmake b/bin/lmake index 5b9cbd107c..c025406806 100755 --- a/bin/lmake +++ b/bin/lmake @@ -98,9 +98,11 @@ def find_lean_opt(): def call_lean(leanfile, options): """ Call lean with options """ from collections import OrderedDict + oleanfile = leanfile[:-5] + ".olean" lean_exe = find_lean_exe() lean_opt = list(OrderedDict.fromkeys(find_lean_opt() + options)) - subprocess.call([lean_exe] + lean_opt + [leanfile], stderr=subprocess.STDOUT) + cmd = [lean_exe] + lean_opt + [leanfile] + ["-o", oleanfile] + subprocess.call(cmd, stderr=subprocess.STDOUT) def get_lean(s): """ Given a string s, return corresponding .lean file if exists """