diff --git a/src/Lean/Compiler/FFI.lean b/src/Lean/Compiler/FFI.lean index 379e17d9f5..d1f4bc5255 100644 --- a/src/Lean/Compiler/FFI.lean +++ b/src/Lean/Compiler/FFI.lean @@ -20,6 +20,6 @@ private constant getBuiltinLinkerFlags (linkStatic : Bool) : String /-- Return linker flags for linking against Lean's libraries. -/ def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) (gmp := "-lgmp") : Array String := - #["-L", (leanSysroot / "lib" / "lean").toString, gmp] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn + #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn ++ [gmp] end Lean.Compiler.FFI