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

feat: turn on warningAsError

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-28 16:51:43 +02:00 • committed by Leonardo de Moura
parent f1f0f60768
commit f4de40d7dc
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
nix/bootstrap.nix
View file

@ -85,6 +85,7 @@ rec {
# use same stage for retrieving dependencies
lean-leanDeps = stage0;
lean-final = self;
leanFlags = [ "-DwarningAsError=true" ];
} ({
src = ../src;
fullSrc = ../.;

2
src/stdlib.make.in
View file

@ -13,7 +13,7 @@ LEANMAKE_OPTS=\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -DwarningAsError=true"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEAN_AR="${CMAKE_AR}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\