From 82d0628065e71985396fdc1ec5265e8e17226304 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Oct 2021 15:53:28 +0200 Subject: [PATCH] fix: leanc: complex LEAN_CC --- src/Leanc.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Leanc.lean b/src/Leanc.lean index 9f779335280e..54a9b951e848 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -42,9 +42,10 @@ Beware of the licensing consequences since GMP is LGPL." let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" if cc.startsWith "." then cc := (binDir / cc).toString - - let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] + -- support `LEANC_CC='ccache cc'` + let cc' :: ccArgs ← cc.trim.splitOn | throw <| IO.userError "LEAN_CC is empty" + let args := ccArgs ++ cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] if args.contains "-v" then - IO.eprintln s!"{cc} {" ".intercalate args}" - let child ← IO.Process.spawn { cmd := cc, args := args.toArray } + IO.eprintln s!"{cc'} {" ".intercalate args}" + let child ← IO.Process.spawn { cmd := cc', args := args.toArray } child.wait