From 15185a1775cd104c4a2dcb95c60a36e984b57258 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 24 Jan 2021 18:58:32 +0100 Subject: [PATCH] fix: unset LEAN_PATH before building stdlib --- src/stdlib.make.in | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 87a4edb28e..8096535c2c 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -1,5 +1,8 @@ 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 # MORE_DEPS: rebuild the stdlib whenever the compiler has changed LEANMAKE_OPTS=\