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

chore(src/CMakeLists,library/Makefile): remove stage1 on clean-olean as well

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-18 19:48:57 +01:00
parent 06695b5942
commit bf5c2ea123
2 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/Makefile.in
View file

@ -29,6 +29,7 @@ depends: $(DEPS)
clean:
find . -name *.olean -delete
find . -name *.depend -delete
find $(STAGE1_DIR) -name *.cpp -delete
$(STAGE1_DIR)/%.cpp: %.lean %.olean
@mkdir -p $(@D)

5
src/CMakeLists.txt
View file

@ -553,11 +553,6 @@ add_custom_target(clean-std-lib
COMMAND make clean
)
add_custom_target(clean-stage1
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
COMMAND "${CMAKE_COMMAND}" -E remove_directory stage1
)
add_custom_target(clean-leanpkg
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg"
COMMAND "${CMAKE_COMMAND}" -P "${CMAKE_MODULE_PATH}/CleanOlean.cmake"