text.append(_names.join(", "))
text.append(" ")
var rest = off - text.length
if rest > 0 then text.append(" " * rest)
text.append(helptext)
#text.append(pretty_default)
text.append(_names.join(", "))
text.append(" ")
var rest = off - text.length
if rest > 0 then text.append(" " * rest)
text.append(helptext)
#text.append(pretty_default)