web2py/web2py — pull request #108 by ilvalle (2013-06-14 07:27:12+00:00)
Title: Editor improvements

- input box for search and open files
- warning message when closing an unsaved files
- buttons to change font-size (useful with projector etc)

tested on FF and Chrome (ubuntu 12.04)