change name

This commit is contained in:
Grahame Grieve 2022-12-20 08:48:55 +13:00
parent 96810c984b
commit e2dff7d118
1 changed files with 1 additions and 1 deletions

View File

@ -60,7 +60,7 @@ public class ProfiledElement {
/**
* @return the short documentation of the definition (shown in the profile table view)
*/
public String shortDoco() {
public String shortDocumentation() {
throw new NotImplementedException("Not done yet");
}