From 12ce18e7e9516cbaf53497e975d9f45ade853fd4 Mon Sep 17 00:00:00 2001
From: Mathieu Durero <durero@kth.se>
Date: Fri, 3 Jun 2022 16:16:05 +0200
Subject: [PATCH] Ignore VSCodium config files

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 19d1ee050..50f4ea1ff 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@ doc.html
 *~
 /_opam
 /Makefile.config
+/.vscode