From d920b78320312112835e541012b17c54d0b843b3 Mon Sep 17 00:00:00 2001
From: ulrich <undisclosed>
Date: Tue, 14 Mar 2017 06:57:26 +0000
Subject: [PATCH] Versuche mit dem Java-Compiler (in Arbeit)
---
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 3b7f34b..2cfd263 100644
--- a/web/ui/ui.js
+++ b/web/ui/ui.js
@@ -845,6 +845,7 @@
lineNumbers: true,
mode: m,
viewportMargin : Infinity,
+ tabSize: 2,
extraKeys: {
"F9": function(cm) {
cm.setOption("fullScreen", !cm.getOption("fullScreen"));
--
Gitblit v1.9.3