diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 8096535c2c..032ae337d7 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -1,7 +1,7 @@ SHELL := /usr/bin/env bash -euo pipefail # any absolute path to the stdlib breaks the Makefile -undefine LEAN_PATH +# 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