Merge branch 'master' into dev_jwt
This commit is contained in:
@@ -57,7 +57,8 @@ feature -- Query
|
|||||||
-- if possible
|
-- if possible
|
||||||
do
|
do
|
||||||
if attached value as v then
|
if attached value as v then
|
||||||
Result := generating_type.name_32
|
-- FIXME: in the future, use the new `{TYPE}.name_32`
|
||||||
|
Result := generating_type.name.to_string_32
|
||||||
else
|
else
|
||||||
Result := {STRING_32} "Void"
|
Result := {STRING_32} "Void"
|
||||||
end
|
end
|
||||||
|
|||||||
Reference in New Issue
Block a user