On Mon, Sep 30, 2019 at 06:33:04AM -0700, Paul Goyette wrote: > If not already done, this should probably be added to src/UPDATING
This is a very generic advice that applies to all updates, and that file is mostly for documenting special update build issues, so I am not sure it is worth an entry for this. Though it has been a rare event lately with such drastic failure, so this might be good enough for an exception. Martin
