Commit graph

2 commits

Author SHA1 Message Date
Tim Landscheidt d9a7da14f1 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
2016-12-25 11:53:20 +00:00
Derk-Jan Hartman 159708754c Adding some gitignore to the math directory, to ignore the compiled binaries and intermediary objects.
Change-Id: Ifcab01b5a67a8da65f8522cc00f2ae00e74a915a
2012-03-25 21:13:52 +02:00