tell gitlab how to highlight files

8de0b894 · Ralf Jung · ae30b2f9 · 8de0b894
Commit 8de0b894 authored Nov 07, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

.gitattributes .gitattributes +1 -0

No files found.
--- a/.gitattributes
+++ b/.gitattributes
+*.v gitlab-language=coq