From a76f4e64f50ecfffcf37119ecaa22e4b7ed298aa Mon Sep 17 00:00:00 2001 From: Dario Vladovic Date: Sun, 21 Jun 2020 14:14:46 +0200 Subject: [PATCH] Add VS Code settings to gitignore --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index 04997db83..e3ca3da4e 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,8 @@ idris2docs_venv # Editor/IDE Related .\#* # Emacs swap file *~ # Vim swap file +# VS Code +.vscode/* /build