From b96c0bdb91ad3bb236eb74d38e9530419cb66eb5 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 5 Sep 2024 15:43:14 +1000 Subject: [PATCH] remove almost-useless .vscode file --- .vscode/settings.json | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 .vscode/settings.json diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 7be5f8ca..00000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,6 +0,0 @@ -{ - "ocaml.sandbox": { - "kind": "opam", - "switch": "default" - } -}