build: simplify clean handling of extras directory

The extras directory is used only as a download target for Mini-OS
sources. Instead of special handling extras/mini-os* in .gitignore and
the clean targets, just use extras for that purpose.

So add "extras" to .gitignore and remove it when doing a
"make distclean".

Signed-off-by: Juergen Gross <jgross@suse.com>

Makefile

@@ -246,6 +246,7 @@ clean-docs:
 # clean, but blow away tarballs
 .PHONY: distclean
 distclean: $(TARGS_DISTCLEAN)
+	rm -rf extras
 	$(MAKE) -C tools/include distclean
 	rm -f config/Toplevel.mk
 	rm -rf dist
@@ -265,7 +266,6 @@ distclean-stubdom:
 ifeq (x86_64,$(XEN_TARGET_ARCH))
 	XEN_TARGET_ARCH=x86_32 $(MAKE) -C stubdom distclean
 endif
-	rm -rf extras/mini-os extras/mini-os-remote
 
 .PHONY: distclean-docs
 distclean-docs: