Merged r14998 from the main 1.3 line as this is essential for the user manual compilation.
The command used was: svn merge -r14997:14998 svn+ssh://bugman@.../svn/relax/1.3
Authored by: bugman 2011-11-14
Parent: [r14998]
Child: [r15000]
