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

chore: reset prefer_native

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-29 13:06:50 +02:00
parent 47c9b740b4
commit ae9b2131c1
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
nix/bootstrap.nix
View file

@ -72,7 +72,7 @@ rec {
src = ../src;
fullSrc = ../.;
inherit debug;
leanFlags = [ "-Dinterpreter.prefer_native=true" ];
leanFlags = [ "-Dinterpreter.prefer_native=false" ];
});
in (all: all // all.lean) rec {
Init = build { name = "Init"; deps = []; };

2
src/stdlib.make.in
View file

@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=true"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\