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

chore: undefine LEAN_PATH

Browse source 
@Kha This doesn't work on my machine. It seems this is a GNU make feature.
This commit is contained in:
Leonardo de Moura 2021-01-24 17:50:05 -08:00
parent f53e83b182
commit 8bc88bde6b
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/stdlib.make.in
View file

@ -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