On Tue, 4 Jul 2017, Carlos O'Donell wrote: > DJ, > > OK to commit with: > > * Two doc changes (see review below). Also regarding documentation: there's a new configure option, so it needs to be added to install.texi, and the INSTALL file regenerated. -- Joseph S. Myers joseph@codesourcery.com