add xml:id attributes wherever we generate the IDs (old patch saved up)

This commit is contained in:
Fred Drake 2004-10-29 19:47:52 +00:00
parent 048840c485
commit 0c1b253fc0
2 changed files with 8 additions and 8 deletions

View file

@ -246,7 +246,7 @@ sub get_version_text() {
sub top_navigation_panel() {
return "\n<div id='top-navigation-panel'>\n"
return "\n<div id='top-navigation-panel' xml:id='top-navigation-panel'>\n"
. make_nav_panel()
. "<hr /></div>\n";
}