diff --git a/src/Leanc.lean b/src/Leanc.lean index 34469aba41..bd5099f024 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -21,10 +21,10 @@ Beware of the licensing consequences since GMP is LGPL." -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn - let cflagsHidden := "@LEANC_INTERNAL_FLAGS@".trim.splitOn + let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn - let ldflagsHidden := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn + let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn for arg in args do match arg with @@ -42,8 +42,14 @@ Beware of the licensing consequences since GMP is LGPL." return 0 | _ => () - let cc := rootify <| (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" - let args := cflags ++ cflagsHidden ++ args ++ ldflagsExt ++ ldflags ++ ldflagsHidden ++ ["-Wno-unused-command-line-argument"] + let mut cc := "@LEANC_CC@" + if let some cc' ← IO.getEnv "LEAN_CC" then + cc := cc' + -- these are intended for the bundled compiler only + cflagsInternal := [] + ldflagsInternal := [] + cc := rootify cc + let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"] let args := args.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}"