From c4643b557277b54a44dccca9e12ebdbd81e850ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Thu, 24 Oct 2019 11:25:00 +0200 Subject: [PATCH] [mdr] move plugin mli into its own gitignore --- .gitignore | 1 - src/plugins/markdown-report/.gitignore | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 4347726a150..6e056235f64 100644 --- a/.gitignore +++ b/.gitignore @@ -209,4 +209,3 @@ hello-*.tar.gz /tests/crowbar/integer_bb_pretty /src/plugins/gui/dgraph_helper.ml /doc/doxygen -/src/plugins/markdown-report/Report_markdown.mli diff --git a/src/plugins/markdown-report/.gitignore b/src/plugins/markdown-report/.gitignore index b43cf1317bc..46c46f82076 100644 --- a/src/plugins/markdown-report/.gitignore +++ b/src/plugins/markdown-report/.gitignore @@ -8,3 +8,4 @@ top/ .merlin *~ /mdr_version.ml +/Report_markdown.mli -- GitLab