diff options
author | Zeger-Jan van de Weg <zegerjan@gitlab.com> | 2016-05-06 18:13:16 +0300 |
---|---|---|
committer | Alfredo Sumaran <alfredo@gitlab.com> | 2016-05-20 23:58:36 +0300 |
commit | fab9dbb3eba55151c34fc8bc171e3670e6c7c422 (patch) | |
tree | c08e23dde57ed18176ea3d7b408c877b81c0fec0 /vendor/gitignore/Coq.gitignore | |
parent | e166a8022a3f239938a1449a0a8ce3485f309766 (diff) |
First import of gitignores
Add .gitignore dropdown when creating a new .gitignore file
Signed-off-by: Alfredo Sumaran <alfredo@gitlab.com>
Diffstat (limited to 'vendor/gitignore/Coq.gitignore')
-rw-r--r-- | vendor/gitignore/Coq.gitignore | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vendor/gitignore/Coq.gitignore b/vendor/gitignore/Coq.gitignore new file mode 100644 index 00000000000..d3083b3a605 --- /dev/null +++ b/vendor/gitignore/Coq.gitignore @@ -0,0 +1,3 @@ +*.vo +*.glob +*.v.d |