Joseph Myers Fri, 25 May 2018 09:36:48 -0700
A new configure option should be documented in install.texi.
-- Joseph S. Myers jos...@codesourcery.com