Re: [lmi] Should we update libxml and its kin?

[Greg Chicares]

On 2022-03-21 12:26, Vadim Zeitlin wrote:
> On Mon, 21 Mar 2022 02:45:30 +0000 Greg Chicares <gchicares@sbcglobal.net> 
> wrote:
[...]
> GC> (A) Move the repository to the free world, i.e., gnu.org .
> GC>     That's too much work just to let me make one change every
> GC>     decade or two. 
> GC> 
> GC> (B) Ask you to commit my patch on github yourself.
> GC> 
> GC> (C) Alter some script (perhaps 'install_xml_libraries.sh')
> GC>     to remove the unwanted file, e.g. [untested]:
[...]
> GC> Between (B) and (C), which would you prefer?
> 
>  (B) seems clearly preferable, so I'll do it if you don't mind.

Thanks.

>  You might get some conflicts with your local changes if I do it

That's okay: I can undo my local changes.

>  Should I do (B) right away?

Yes, please.