[web2py] change the encoding

[Jose]

Hi,

How can I change the encoding of the files edited with the editor's
own web2py?

Rgards,
Jose