Re: Fwd: bug#34220: failure to building with CompCert, patch proposed

[Bruno Haible]

Paul Eggert answered in <https://debbugs.gnu.org/cgi/bugreport.cgi?bug=34220>.