max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lake: rm excess -lstdcpp from FFI example (#7758)

Browse source 
This PR removes the `-lstdcpp` extra link argument from the FFI example.
It is not actually necessary.
This commit is contained in:
Mac Malone 2025-03-31 23:10:54 -04:00 • committed by GitHub
parent 34142685a9
commit 7fefa8660e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/lake/examples/ffi/lib/lakefile.lean
View file

@ -50,4 +50,3 @@ target libleanffi_shared pkg : Dynlib := do
lean_lib FFI.Shared where
moreLinkLibs := #[libleanffi_shared]
moreLinkArgs := #["-lstdc++"]