[Bug 31016] HTML Help does not properly handle index entries with the same name