Commit 7696e337ee77685f48f7b805afa44a5dec3cc78e

Werner Lemberg 2015-11-26T14:31:08

Use new docmaker syntax for identifiers with identical names.