From 9b0eef430e721c58fcfb6377d1f4f01b93312a7b Mon Sep 17 00:00:00 2001
From: Gerolf Ziegenhain <gerolf.ziegenhain@gmail.com>
Date: Sat, 27 Jan 2024 18:09:26 +0100
Subject: [PATCH] ignore build dirs

---
 .gitignore               |  3 +++
 DroidStar.code-workspace | 10 ++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 DroidStar.code-workspace

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c1f3e08
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+.DS_Store
+build/*
+build_*/*
\ No newline at end of file
diff --git a/DroidStar.code-workspace b/DroidStar.code-workspace
new file mode 100644
index 0000000..fd3b45f
--- /dev/null
+++ b/DroidStar.code-workspace
@@ -0,0 +1,10 @@
+{
+	"folders": [
+		{
+			"path": "."
+		}
+	],
+	"settings": {
+		"git.ignoreLimitWarning": true
+	}
+}
\ No newline at end of file