dot/jupyter-notebook.json: Set `tabSize' because the editor is broken.
authorMark Wooding <mdw@distorted.org.uk>
Tue, 11 Apr 2023 12:00:01 +0000 (13:00 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Tue, 11 Apr 2023 12:00:01 +0000 (13:00 +0100)
commit0b02a1130cab28f267f4f12a66c4de2ead4ce578
treec9029d7b6569a0f17c783557f498af119985f8eb
parent6f4c361e28c171aa7ecb634c6ed93d476a73fb4b
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