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

chore: fix typo in CLI usage (--ldlags) (#1947)

Browse source
This commit is contained in:
locriacyber 2022-12-14 09:20:50 +00:00 • committed by GitHub
parent 4fa8d003d8
commit fa761b8baf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Leanc.lean
View file

@ -12,7 +12,7 @@ as-is to the wrapped compiler.
Interesting options:
* `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit
* `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit"
* `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit"
return 1
let root ← match (← IO.getEnv "LEAN_SYSROOT") with