Ignore binary files from examples

anoma · Dec 5, 2022 · 6534287 · 6534287
1 parent 2db738a
commit 6534287
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/.gitignore b/.gitignore
@@ -82,5 +82,7 @@ docs/**/*.md
 *.cmi
 *.cmx
 *.cmo
-
+.history
 docs/org/README.org
+# Binary files (produced by `make check`)
+examples/milestone/HelloWorld/HelloWorld