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

chore: do not remove stage0 build on clean-olean

Browse source 
/cc @leodemoura
This commit is contained in:
Sebastian Ullrich 2019-12-16 13:18:57 +01:00
parent a1aac9a98d
commit fc964fb08d
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/CMakeLists.txt
View file

@ -621,7 +621,7 @@ add_custom_target(clean-stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init"
COMMAND find . -name '*.olean' -delete
COMMAND find . -name '*.depend' -delete
COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage*" || true
COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
)
add_custom_target(clean-olean