DynamoRIO / DynamoRIO/dynamorio

docs: eliminate duplicate top-level navbar entry

Open
#918 0 comments 0 reactions 0 assignees View on GitHub
Component-Docs Migrated Priority-Medium
Dominant language
C
Stars
3.2k
Forks
629
Avg merge
2d 15h
Merged PRs (30d)
31

Description

_From [bruen...@google.com](https://code.google.com/u/109494838902877177630/) on September 24, 2012 13:41:59_

the navbar has a plain initial entry w/ the name of the main_page: "The
DynamoRIO API", or "Dr. Memory". then it has a duplcate entry w/ the same
name that expands.

in navtree.js:
var NAVTREE =
[
[ "DynamoRIO API", "index.html", [
[ "The DynamoRIO API", "index.html", null ],
[ "The DynamoRIO API", "index.html", "index" ],

I tried just removing the no-child entry:
# get rid of the duplicate top-level entry
string(REGEX MATCH "\[ \"[^\"]*\", \"index.html\", \"index\" \]" top "${string}")
if (top)
string(REPLACE ", \"index\" ]" "" top "${top}")
string(REPLACE "[" "" top "${top}")
string(REGEX REPLACE
"\[${top}, null \],\n\r? *\[${top}, \"index\" \]"
"[${top}, \"index\" ]"
string "${string}")
endif (top)

but the navigation gets all messed up, b/c it uses files and vars w/ names
equal to indices in the top-level tree:
> l api/docs/html/nav*
4 api/docs/html/nav_f.png 20 api/docs/html/navtreeindex1.js 20 api/docs/html/navtreeindex6.js 16 api/docs/html/navtree.js
4 api/docs/html/nav_g.png 20 api/docs/html/navtreeindex2.js 20 api/docs/html/navtreeindex7.js 16 api/docs/html/navtree.js~
4 api/docs/html/nav_h.png 20 api/docs/html/navtreeindex3.js 16 api/docs/html/navtreeindex8.js
4 api/docs/html/navtree.css 20 api/docs/html/navtreeindex4.js 12 api/docs/html/navtreeindex9.js
16 api/docs/html/navtreeindex0.js 20 api/docs/html/navtreeindex5.js 4 api/docs/html/navtreeindex.js

I tried adjusting the indices but my code change didn't work so I gave up.

_Original issue: http://code.google.com/p/dynamorio/issues/detail?id=918_

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.