From d27c85e30c62d4e2a611603fed1784e1fd415370 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Aug 2014 10:11:01 -0700 Subject: [PATCH] fix(library/Makefile.common): avoid error message when .d files do not exist Signed-off-by: Leonardo de Moura --- library/Makefile.common | 2 +- src/CMakeLists.txt | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/library/Makefile.common b/library/Makefile.common index 6912530f7..8512a7552 100644 --- a/library/Makefile.common +++ b/library/Makefile.common @@ -20,7 +20,7 @@ all: $(OLEAN_FILES) $(DEP_FILES) @rm -f $@.tmp.1 @rm -f $@.tmp.2 -include $(LEAN_FILES:.lean=.d) +-include $(LEAN_FILES:.lean=.d) .PHONY: all clean diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9da0e7bcc..f8fc99441 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -328,4 +328,9 @@ endif() add_custom_target(clean-olean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library COMMAND find . -name '*.olean' -exec rm -f '{}' '\;' -) \ No newline at end of file + ) + +add_custom_target(clean-d + WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library + COMMAND find . -name '*.d' -exec rm -f '{}' '\;' + ) \ No newline at end of file