-
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>
9589296e