diff options
Diffstat (limited to 'Utilities/Sphinx/create_identifiers.py')
-rwxr-xr-x | Utilities/Sphinx/create_identifiers.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Utilities/Sphinx/create_identifiers.py b/Utilities/Sphinx/create_identifiers.py index 7715e53..3fe3fcb 100755 --- a/Utilities/Sphinx/create_identifiers.py +++ b/Utilities/Sphinx/create_identifiers.py @@ -34,7 +34,7 @@ for line in lines: for domain_object_string, domain_object_type in mapping: if "<keyword name=\"" + domain_object_string + "\"" in line: - if not "id=\"" in line: + if not "id=\"" in line and not "#index-" in line: prefix = "<keyword name=\"" + domain_object_string + "\" " part1, part2 = line.split(prefix) head, tail = part2.split("#" + domain_object_type + ":") |