horse: finish rename of trainee -> uma in koka
This commit is contained in:
@@ -193,11 +193,11 @@ pub fun activations(s: skill-id): list<activation>
|
||||
// Get the owner of a unique skill.
|
||||
// If the skill is not unique, or if there is no skill with the given ID,
|
||||
// the result is Nothing.
|
||||
pub fun unique-owner(s: skill-id): maybe<trainee-id>
|
||||
pub fun unique-owner(s: skill-id): maybe<uma-id>
|
||||
match s.game-id
|
||||
{{- range $s := $.Skills }}
|
||||
{{- if $s.UniqueOwnerID }}
|
||||
{{ $s.ID }} -> Just(Trainee-id({{ $s.UniqueOwnerID }}))
|
||||
{{ $s.ID }} -> Just(Uma-id({{ $s.UniqueOwnerID }}))
|
||||
{{- end }}
|
||||
{{- end }}
|
||||
_ -> Nothing
|
||||
|
||||
Reference in New Issue
Block a user