1. 2010-03-26 [3] [Bug-dejagnu] Error in doc/user.xml makes manual unprocessable dejagnu-bug Rainer Orth