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

fix: unset LEAN_PATH before building stdlib

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-24 18:58:32 +01:00
parent b15e770231
commit 15185a1775
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/stdlib.make.in
View file

@ -1,5 +1,8 @@
SHELL := /usr/bin/env bash -euo pipefail SHELL := /usr/bin/env bash -euo pipefail
# any absolute path to the stdlib breaks the Makefile
undefine LEAN_PATH
# LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage
# MORE_DEPS: rebuild the stdlib whenever the compiler has changed # MORE_DEPS: rebuild the stdlib whenever the compiler has changed
LEANMAKE_OPTS=\ LEANMAKE_OPTS=\