fix: LEAN_PATH example
This commit is contained in:
parent
77b517f4c6
commit
4abe2fa72f
|
@ -81,7 +81,7 @@ the environment might be setup like this:
|
||||||
``` sh
|
``` sh
|
||||||
LIB="../lib"
|
LIB="../lib"
|
||||||
LIB_MATHLIB="$LIB/mathlib4/.lake"
|
LIB_MATHLIB="$LIB/mathlib4/.lake"
|
||||||
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
|
export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
|
||||||
|
|
||||||
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
||||||
```
|
```
|
||||||
|
|
Loading…
Reference in New Issue