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