Don't show hints in diffs

FStarLang · Jul 9, 2019 · d6f2fc2 · d6f2fc2
1 parent 01eafeb
commit d6f2fc2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.gitattributes b/.gitattributes
@@ -3,4 +3,4 @@
 *.c eol=lf
 *.h eol=lf
 Makefile eol=lf
-*.hints -diff
+*.hints eol=lf -diff linguist-generated