ignore build dirs
This commit is contained in:
parent
bd73d8f26f
commit
9b0eef430e
2 changed files with 13 additions and 0 deletions
3
.gitignore
vendored
Normal file
3
.gitignore
vendored
Normal file
|
@ -0,0 +1,3 @@
|
||||||
|
.DS_Store
|
||||||
|
build/*
|
||||||
|
build_*/*
|
10
DroidStar.code-workspace
Normal file
10
DroidStar.code-workspace
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
{
|
||||||
|
"folders": [
|
||||||
|
{
|
||||||
|
"path": "."
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"settings": {
|
||||||
|
"git.ignoreLimitWarning": true
|
||||||
|
}
|
||||||
|
}
|
Loading…
Add table
Reference in a new issue