fix: leanc: complex LEAN_CC

leanprover · Oct 6, 2021 · 2c3e1a3 · 2c3e1a3
1 parent d9f887b
commit 2c3e1a3
Showing 1 changed file with 5 additions and 4 deletions.
diff --git 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