Use names instead of ids for wiki anchors (#6905).
Authored by: jplang 2011-03-14
Parent: [r5134]
Child: [r5136]