From e034aaaafed79cfcc3fbd4c50c06ffc34b250b9d Mon Sep 17 00:00:00 2001
From: ulrich <undisclosed>
Date: Mon, 20 Mar 2017 16:08:09 +0000
Subject: [PATCH] log-Einstellungen geaendert
---
web/ui/ui.js | 1 +
1 files changed, 1 insertions(+), 0 deletions(-)
diff --git a/web/ui/ui.js b/web/ui/ui.js
index d01cf03..3deda97 100644
--- a/web/ui/ui.js
+++ b/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) {
--
Gitblit v1.9.3