From 12306ba401ef67202abda4df6cebb370666392a0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 23 Nov 2021 09:33:06 +0100 Subject: [PATCH] fix: -lgmp should come last --- src/Lean/Compiler/FFI.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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