aboutsummaryrefslogtreecommitdiffstats
path: root/.gitattributes
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-09-19 18:05:04 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-09-19 18:05:04 +0100
commita56c0bd55f921f85ddbb8b02c2f4c7ac89bf3aaf (patch)
treee0a727e7286bd8199315764aaf9713c35513f606 /.gitattributes
parent963aff77e8cb73116bdc4b0250dbd61c787159d2 (diff)
parent660f82f83c18c672d486baa3429e19a7b77ab4fb (diff)
downloadvericert-a56c0bd55f921f85ddbb8b02c2f4c7ac89bf3aaf.tar.gz
vericert-a56c0bd55f921f85ddbb8b02c2f4c7ac89bf3aaf.zip
Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalis
Diffstat (limited to '.gitattributes')
-rw-r--r--.gitattributes2
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitattributes b/.gitattributes
index 30dd12d..8c19733 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,4 +1,4 @@
*.h linguist-language=C
*.c linguist-language=C
*.v linguist-language=Coq
-benchmarks/* linguist-vendored
+benchmarks/** linguist-vendored