e2a4dd7
Removed develop.js. The develop.js is no longer necessary because the code in it has been merged into the main code. An empty extension.js has been added to provide a place for UI customization. Ticket #2099