whoops, what a mess

github-linguist · Nov 22, 2023 · 6594d71 · 6594d71
1 parent 9fa2c11
commit 6594d71
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1338,6 +1338,3 @@
 [submodule "vendor/grammars/zephir-sublime"]
 	path = vendor/grammars/zephir-sublime
 	url = https://github.com/phalcon/zephir-sublime
-[submodule "vendor/vscode-lean4"]
-	path = vendor/vscode-lean4
-	url = https://github.com/leanprover/vscode-lean4
diff --git a/vendor/vscode-lean4 b/vendor/vscode-lean4