jenkins-bot has submitted this change and it was merged. ( https://gerrit.wikimedia.org/r/329126 )
Change subject: Do not ignore .mli files ...................................................................... Do not ignore .mli files The pattern "*.mli" was incorrectly added to math/.gitignore by 159708754ce957fb9931dbdd5bb69a309aada69e 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 --- M math/.gitignore 1 file changed, 0 insertions(+), 1 deletion(-) Approvals: jenkins-bot: Verified TheDJ: Looks good to me, approved diff --git a/math/.gitignore b/math/.gitignore index cac42e2..18dc1ad 100644 --- a/math/.gitignore +++ b/math/.gitignore @@ -1,5 +1,4 @@ # Compiled source -*.mli *.cmi *.cmx *.o -- To view, visit https://gerrit.wikimedia.org/r/329126 To unsubscribe, visit https://gerrit.wikimedia.org/r/settings Gerrit-MessageType: merged Gerrit-Change-Id: I1eee6b46f8f81a7a0085901f602eb7a1f4ae6fd4 Gerrit-PatchSet: 1 Gerrit-Project: mediawiki/extensions/Math Gerrit-Branch: master Gerrit-Owner: Tim Landscheidt <t...@tim-landscheidt.de> Gerrit-Reviewer: Chad <ch...@wikimedia.org> Gerrit-Reviewer: Physikerwelt <w...@physikerwelt.de> Gerrit-Reviewer: TheDJ <hartman.w...@gmail.com> Gerrit-Reviewer: Tim Landscheidt <t...@tim-landscheidt.de> Gerrit-Reviewer: jenkins-bot <> _______________________________________________ MediaWiki-commits mailing list MediaWiki-commits@lists.wikimedia.org https://lists.wikimedia.org/mailman/listinfo/mediawiki-commits