Skip to content

Commit cc0e884

Browse files
authored
fix config (#201)
1 parent f22935b commit cc0e884

2 files changed

Lines changed: 3 additions & 3 deletions

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 ! -path $(ROOT_PATH)/%) -delete; fi
410410

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

config

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -170,9 +170,9 @@ then
170170
echo create deps.mk ...
171171
rm -f deps.mk
172172
touch deps.mk
173-
set $base_rocqfiles
174-
if test $# -gt 0
173+
if test -n "$base_rocqfiles"
175174
then
175+
set $base_rocqfiles
176176
echo -n ${1}o >> deps.mk
177177
shift
178178
for f in $*

0 commit comments

Comments
 (0)