aboutsummaryrefslogtreecommitdiffstats
path: root/.gitattributes
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-07-20 11:51:34 +0100
committerYann Herklotz <git@yannherklotz.com>2020-07-20 11:51:34 +0100
commit9c6a88c1d3896f30874a4965b98b33de6b98838a (patch)
treec5dd585a529664a67a0ced131507fd3352ed9270 /.gitattributes
parente76d47379c0653312deb076237271a7c308c60d1 (diff)
downloadvericert-9c6a88c1d3896f30874a4965b98b33de6b98838a.tar.gz
vericert-9c6a88c1d3896f30874a4965b98b33de6b98838a.zip
Add .gitattributes
Diffstat (limited to '.gitattributes')
-rw-r--r--.gitattributes3
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000..5076ac1
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,3 @@
+*.h linguist-language=C
+*.c linguist-language=C
+*.v linguist-language=Coq