Dateiverwaltung für die WebBox
Ulrich
2020-11-20 9778400996a77ca6118c4ed6857d9ced33dcf14b
web/ui/ui.js
@@ -74,6 +74,7 @@
  $('#m-test-3').on('click', fm_menu_compile_all);
  $('#m-compile-results').on('click', fm_fusszeile_zeigen);
  $('#m-build-app').on('click', fm_menu_build_app);
  $('#m-ant-build').on('click', fm_menu_ant_build);
  $('#saveModal').on('hidden.bs.modal', function (e) {
    $('#modal_ok').attr('onclick','').unbind('click');
  });
@@ -345,6 +346,10 @@
  fm_build_app();
}
function fm_menu_ant_build() {
  fm_ant_build();
}
function fm_mark_compile_results_in_editor(resp) {
  cm.clearGutter("breakpoints");