From 658674fb8cae60a9ef53c9dd8592d75a195c7e78 Mon Sep 17 00:00:00 2001 From: "Hanwen (Steinway) Wu" Date: Thu, 8 Sep 2016 15:25:22 -0400 Subject: [PATCH] use tab instead of soft tab Hi @prasmussen, this is related to https://github.com/prasmussen/glot/issues/5. I propose this change to make tabs tabs, instead of 4 spaces, but it is up to you. Hard tabs makes it easier to write makefiles. --- templates/widgets/editor.julius | 1 + 1 file changed, 1 insertion(+) diff --git a/templates/widgets/editor.julius b/templates/widgets/editor.julius index bda51ff..a25d558 100644 --- a/templates/widgets/editor.julius +++ b/templates/widgets/editor.julius @@ -9,6 +9,7 @@ window.Editor = (function() { editor.setTheme(theme); editor.setKeyboardHandler(keybindings); editor.getSession().setMode(#{toJSON $ languageAceMode lang}); + editor.getSession().setUseSoftTabs(false); editor.setOptions({ minLines: lineCount, maxLines: lineCount,