@ -763,6 +763,7 @@
editor.getSession().on('change', onChange);
editor.on('changeSession', function(){
onChange();
})
document.querySelector('#optimize').addEventListener('change', function(){