aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-08-18 18:47:55 +0200
committerGuillaume Melquiond2016-08-18 18:47:55 +0200
commit262ad3c3ce24463094110aa011471213ac0b61c7 (patch)
tree937fc304508e241871ef6050db53f9fec8850e99 /dev/include
parent86935e33e8f5d4fcc4b5603086d594431a002d0b (diff)
Fix incorrect glob data for module symbols (bug #2336).
The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions