[tor-bugs] #21376 [Metrics]: add javadoc metrics style

[Tor Bug Tracker & Wiki]

#21376: add javadoc metrics style
-------------------------+------------------------------
 Reporter:  iwakeh       |          Owner:  metrics-team
     Type:  enhancement  |         Status:  assigned
 Priority:  Medium       |      Milestone:
Component:  Metrics      |        Version:
 Severity:  Normal       |     Resolution:
 Keywords:               |  Actual Points:
Parent ID:               |         Points:
 Reviewer:               |        Sponsor:
-------------------------+------------------------------
Changes (by RaBe):

 * owner:  RaBe => metrics-team


Comment:

 I did not even touch the font of the default JavaDoc stylesheet :) But I
 agree with it being the mentioned known bug, so you can just remove the
 import line. On systems that have Deja Vu installed it will still be
 displayed, for other systems it falls back to Arial, which should be fine!

--
Ticket URL: <https://trac.torproject.org/projects/tor/ticket/21376#comment:8>
Tor Bug Tracker & Wiki <https://trac.torproject.org/>
The Tor Project: anonymity online