How to change the file extension of generated doc files

[Jeremy DeHaan via Digitalmars-d-learn]

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.