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
diff --git a/deps/Makefile b/deps/Makefile
index ccf2bdb..1d9a6e6 100644
--- a/deps/Makefile
+++ b/deps/Makefile
@@ -58,7 +58,11 @@
(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