Pdflatex is the recommended export tool for the manuals.
Pdflatex brings the best results for hyperlinking.
Some features (e.g. rotated text) are not available in DVI or PS (dvips).
This does not affect export from command line or autotests
(where this setting is ignored and the format must aways be given explicitely).