From 2bf87074e17e77ca761e3490e5f054175e082e5b Mon Sep 17 00:00:00 2001 From: Daniel Kiper Date: Tue, 7 May 2013 13:51:41 +0200 Subject: stubdom: Clean extras/mini-os directory during make clean Signed-off-by: Daniel Kiper Acked-by: Samuel Thibault --- stubdom/Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'stubdom') diff --git a/stubdom/Makefile b/stubdom/Makefile index a2ac044833..91e2e1ae96 100644 --- a/stubdom/Makefile +++ b/stubdom/Makefile @@ -498,6 +498,7 @@ clean: rm -fr mini-os-$(XEN_TARGET_ARCH)-xenstore rm -fr mini-os-$(XEN_TARGET_ARCH)-vtpm rm -fr mini-os-$(XEN_TARGET_ARCH)-vtpmmgr + $(MAKE) DESTDIR= -C $(MINI_OS) clean $(MAKE) DESTDIR= -C caml clean $(MAKE) DESTDIR= -C c clean $(MAKE) -C vtpm clean -- cgit v1.2.3