made building user doc optional at configure time
Authored by: Jean-Francois Dockes 2015-08-23
Parent(s): [d8e8ce]
Child(ren): [766a34]