From 994815bc7793f5765beb693c82341cf01d20d807 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 15 Feb 2016 14:31:15 -0500 Subject: [PATCH] fix(bin/linja.in): roll back d8fb6f5 The previous fix d8fb6f5 creates a problem in Linux platform. Related issue: #986 --- bin/linja.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/linja.in b/bin/linja.in index 0775d171c0..309fdf9fc5 100755 --- a/bin/linja.in +++ b/bin/linja.in @@ -414,7 +414,7 @@ def get_lean_options(args): if args.to_axiom: args.lean_options.append("--to_axiom") if args.cache: - args.lean_options += ["-c", '"%s"' % args.cache] + args.lean_options += ["-c", '%s' % args.cache] if args.lean_config_option: for item in args.lean_config_option: args.lean_options.append("-D" + item)