deps/Makefile: Separate 'distclean' from 'clean'
'distclean' removes the actual git clones, while 'clean' now simply ensures that there are no local changes between to index. Change-Id: I5de68644b397ff7fbca0595a8900b41508d59bde
This commit is contained in:
parent
981be73b1c
commit
4c294b6d46
|
@ -58,7 +58,11 @@ $(1)/update: $(1)
|
|||
(cd $(1) && git remote set-url origin $(2)/$(1) && git fetch && git checkout -f -B master origin/master)
|
||||
|
||||
.PHONY: $(1)/clean
|
||||
$(1)/clean:
|
||||
$(1)/clean: $(1)
|
||||
(cd $(1) && git checkout -f -B master && git reset --hard)
|
||||
|
||||
.PHONY: $(1)/distclean
|
||||
$(1)/distclean:
|
||||
@rm -rf $(1)
|
||||
endef
|
||||
|
||||
|
|
Loading…
Reference in New Issue