diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-09-30 17:26:21 +0200 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-09-30 17:32:25 +0200 |
commit | a8586f12b75687061a6d8df9d23696d35f4472f0 (patch) | |
tree | 2bdd14dd04b5d861414dfaf569f7ed4712373507 /.gitattributes | |
parent | b5b154620e454ba947957eb1164acbffff1cb5bd (diff) | |
download | compcert-a8586f12b75687061a6d8df9d23696d35f4472f0.tar.gz compcert-a8586f12b75687061a6d8df9d23696d35f4472f0.zip |
Added .gitattributes file.
Treat doc as documentation and tests as vendored for github linguist
Diffstat (limited to '.gitattributes')
-rw-r--r-- | .gitattributes | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 00000000..02ab53c1 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,3 @@ +# Files that should be ignored by Github linguist +test/* linguist-vendored +doc/* linguist-documentation |