diff options
| author | Guillermo Ramos | 2014-02-26 20:08:11 +0100 |
|---|---|---|
| committer | Guillermo Ramos | 2014-02-26 20:08:11 +0100 |
| commit | 9811c02fddca07f88f010ad3d62e6de7db5b244f (patch) | |
| tree | 76ba3c940e2dc7eb4e0ade46a4bdad017fd67614 /.gitignore | |
| parent | c33222a061c3087700e743bc3e3f8cdaf3ce4f9d (diff) | |
| download | witch-9811c02fddca07f88f010ad3d62e6de7db5b244f.tar.gz | |
Initial commit 2
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 12 |
1 files changed, 3 insertions, 9 deletions
@@ -1,9 +1,3 @@ -*.annot -*.cmo -*.cma -*.cmi -*.a -*.o -*.cmx -*.cmxs -*.cmxa +_build +*.native +*.byte |