stubdom: Clean extras/mini-os directory during make clean

Signed-off-by: Daniel Kiper <daniel.kiper@oracle.com>
Acked-by: Samuel Thibault <samuel.thibault@ens-lyon.org>

diff --git a/stubdom/Makefile b/stubdom/Makefile
index a2ac04483363878f885d99b63a8e1b15668416ac..91e2e1ae9653d3494406f63fe1c8fb451f7e7bff 100644 (file)
--- 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