Git Attributes (#1373)

hazelgrove · Aug 16, 2024 · e9750bf · e9750bf
2 parents a348fd0 + a136739
commit e9750bf
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/.gitattributes b/.gitattributes
@@ -2,3 +2,11 @@
 # decides that the content is text, its line endings are converted to LF on
 # checkin. When the file has been committed with CRLF, no conversion is done.
 * text=auto
+
+
+# Mark generated code and documentation as such to exclude them from PR diffs and stats.
+# More information: https://github.com/github-linguist/linguist/blob/master/docs/overrides.md#generated-code
+src/haz3lweb/Init.ml linguist-generated
+src/haz3lweb/exercises/**/*.ml linguist-generated
+*.md linguist-documentation
+docs/** linguist-documentation