diff --git a/Makefile b/Makefile index 83f4e0d..1089bb8 100644 --- a/Makefile +++ b/Makefile @@ -406,7 +406,7 @@ clean-lean: rm-lean .PHONY: rm-lean rm-lean: - if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -name $(ROOT_PATH)/%) -delete; fi + if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -path $(ROOT_PATH)/%) -delete; fi $(ROOT_PATH).lean: ifneq ($(SET_STI_FILES),1) diff --git a/config b/config index 2ad035d..32fdb66 100755 --- a/config +++ b/config @@ -170,9 +170,9 @@ then echo create deps.mk ... rm -f deps.mk touch deps.mk - set $base_rocqfiles - if test $# -gt 0 + if test -n "$base_rocqfiles" then + set $base_rocqfiles echo -n ${1}o >> deps.mk shift for f in $*