On 23.08.2023 10:39, Juergen Gross wrote: > 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 <[email protected]>
Acked-by: Jan Beulich <[email protected]> of course with ... > --- > .gitignore | 2 +- > .hgignore | 6 +----- > Makefile | 2 +- > 3 files changed, 3 insertions(+), 7 deletions(-) ... the no longer applicable .hgignore hunk dropped. > --- a/Makefile > +++ b/Makefile > @@ -246,6 +246,7 @@ clean-docs: > # clean, but blow away tarballs > .PHONY: distclean > distclean: $(TARGS_DISTCLEAN) > + rm -rf extras I'd also be inclined to add a trailing / here, but I guess I'll better leave the change untouched while committing. Jan
