I can't find anywhere describing how to change the extension of the generated doc files.

I've tried `-ofxxxx.php`, but it still generates xxxx.html.

I'm probably missing something here that's going to make me feel silly.