On Thu, Dec 12, 2019 at 06:30:43PM +0000, Andrew Cooper wrote: > On 12/12/2019 18:27, Anthony PERARD wrote: > > diff --git a/docs/misc/distro_mapping.txt b/docs/misc/distro_mapping.txt > > index 2e46592728e3..599b6fd1e912 100644 > > --- a/docs/misc/distro_mapping.txt > > +++ b/docs/misc/distro_mapping.txt > > It looks like this is entirely obsolete since we switched to using > ./configure. > > Mind if we expand the patch to kill this file fully? (Can be sorted on > commit if you want.)
I think it would be better to remove the file in a separated commit, with a proper explanation. Probably about half of the file is still true, I'm not sure about the other half. That document might not be relevant anymore, since hopefully ./configure --help is enough, but I haven't checked. Thanks, -- Anthony PERARD _______________________________________________ Xen-devel mailing list Xen-devel@lists.xenproject.org https://lists.xenproject.org/mailman/listinfo/xen-devel
