log-Einstellungen geaendert

ulrich

2017-03-20 e034aaaafed79cfcc3fbd4c50c06ffc34b250b9d

 web/ui/ui.js

@@ -338,6 +338,7 @@
  cm.clearGutter("breakpoints");

  if(resp.List[0].CompilerIssue !== undefined) {
    cm.setGutterMarker(0, "breakpoints", makeMarker("Code hat Fehler"));
    var lno;
    var eMsg;
    if(resp.List[0].CompilerIssue instanceof Array) {