> > make html works fine, as far as I can tell. Is there any reason why> this ticket can't be rejected?
No. Deleted those two comments in r38663. Marking ticket rejected.
kid51