On 4/3/20, David Kastrup <d...@gnu.org> wrote: > Anybody have an idea whose Patchy pushed the following: > commit f5f907599ce88d3d610483fa42fa78be12f53d2e
Uh, I did push it onto staging after the usual review process. Could that really be what broke some stuff? It’s a fairly simple documentation edit… (Unlike my latest patches, that do make some regtest changes, but none of these have reached staging yet.) V.
