Do not ignore .mli files

The pattern "*.mli" was incorrectly added to math/.gitignore by
159708754c with the comment "Compiled
source".  Actually, .mli files define the interfaces for the
corresponding .ml module.  They are manually created and maintained,
akin to .h files in C, and thus changes to them should not be ignored.

Change-Id: I1eee6b46f8f81a7a0085901f602eb7a1f4ae6fd4
This commit is contained in:
Tim Landscheidt 2016-12-25 11:44:32 +00:00
parent 513372bae2
commit d9a7da14f1

1
math/.gitignore vendored
View File

@ -1,5 +1,4 @@
# Compiled source
*.mli
*.cmi
*.cmx
*.o