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
