Properly document hotkeys in generated documentation.#15037

Merged

bors merged 1 commit intorust-lang:masterfrom

zzmp:doc/hotkeys

Jun 19, 2014

Commits on Jun 19, 2014

(doc) Properly doc hotkeys in generated docs.
zzmp
committed