diff options
Diffstat (limited to 'stubdom/Makefile')
| -rw-r--r-- | stubdom/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
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 |