From 801fde05523c1de797f7ddb966fedcd6ac477e12 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 22 Oct 2019 13:30:34 +0200 Subject: [PATCH] [MdR] ignore generated API module --- .gitignore | 1 + src/plugins/markdown-report/Makefile | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 6e056235f64..4347726a150 100644 --- a/.gitignore +++ b/.gitignore @@ -209,3 +209,4 @@ 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/Makefile b/src/plugins/markdown-report/Makefile index 12c2879b68e..a92ec35f6a8 100644 --- a/src/plugins/markdown-report/Makefile +++ b/src/plugins/markdown-report/Makefile @@ -5,7 +5,7 @@ endif Report_markdown_VERSION:=0.1~beta PLUGIN_NAME:=Report_markdown -PLUGIN_GENERATED:=$(PLUGIN_DIR)/mdr_version.ml +PLUGIN_GENERATED:=$(PLUGIN_DIR)/mdr_version.ml $(PLUGIN_DIR)/Report_markdown.mli PLUGIN_CMO:=\ sarif mdr_version mdr_params parse_remarks \ eva_coverage md_gen sarif_gen mdr_register -- GitLab