remove micro dots, don't need that
icyphox icyph0x@protonmail.com
Sun, 21 Jan 2018 20:37:33 +0530
D
micro/.config/micro/settings.json
@@ -1,35 +0,0 @@
-{ - "autoclose": true, - "autoindent": true, - "autosave": false, - "colorcolumn": 0, - "colorscheme": "simple", - "cursorline": true, - "eofnewline": false, - "ftoptions": true, - "ignorecase": false, - "indentchar": " ", - "infobar": true, - "keepautoindent": false, - "linter": true, - "pluginchannels": [ - "https://raw.githubusercontent.com/micro-editor/plugin-channel/master/channel.json" - ], - "pluginrepos": [], - "rmtrailingws": false, - "ruler": true, - "savecursor": false, - "saveundo": false, - "scrollmargin": 3, - "scrollspeed": 2, - "softwrap": false, - "splitBottom": true, - "splitRight": true, - "statusline": true, - "syntax": true, - "tabmovement": false, - "tabsize": 4, - "tabstospaces": false, - "termtitle": false, - "useprimary": true -}