From 0b02a1130cab28f267f4f12a66c4de2ead4ce578 Mon Sep 17 00:00:00 2001
From: Mark Wooding <mdw@distorted.org.uk>
Date: Tue, 11 Apr 2023 13:00:01 +0100
Subject: [PATCH] dot/jupyter-notebook.json: Set `tabSize' because the editor
 is broken.

The thing which handles deleting indentation when you press backspace
quantizes to the tab size, not the indentation unit, which is obviously
wrong.  Fortunately, I don't think I care what it thinks the tab size
is, so set it to match the indent unit.
---
 dot/jupyter-notebook.json | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/dot/jupyter-notebook.json b/dot/jupyter-notebook.json
index ebf4aae..e84b6e2 100644
--- a/dot/jupyter-notebook.json
+++ b/dot/jupyter-notebook.json
@@ -2,7 +2,8 @@
   "CodeCell": {
     "cm_config": {
       "autoCloseBrackets": false,
-      "indentUnit": 2
+      "indentUnit": 2,
+      "tabSize": 2
     }
   }
 }
-- 
2.11.0