Skip to content

Commit 6019323

Browse files
committed
wip
1 parent fe7f149 commit 6019323

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -406,7 +406,7 @@ clean-lean: rm-lean
406406

407407
.PHONY: rm-lean
408408
rm-lean:
409-
if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -name $(ROOT_PATH)/%) -delete; fi
409+
if test -d $(ROOT_PATH); then find $(ROOT_PATH) -maxdepth 1 -name '*.lean' $(LEANFILES:%=-a ! -wholename $(ROOT_PATH)/%) -delete; fi
410410

411411
$(ROOT_PATH).lean:
412412
ifneq ($(SET_STI_FILES),1)

0 commit comments

Comments
 (0)