From 2ae3b763b524c362132a3cbfc6bc9f03ee843f47 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 15 Oct 2019 14:50:08 +0200 Subject: [PATCH] [mdr] fixes missing PLUGIN_DIR prefixes --- src/plugins/markdown-report/Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/plugins/markdown-report/Makefile b/src/plugins/markdown-report/Makefile index 3c39dd629b4..da516324671 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:=mdr_version.ml +PLUGIN_GENERATED:=$(PLUGIN_DIR)/mdr_version.ml PLUGIN_CMO:=\ markdown sarif mdr_version mdr_params parse_remarks \ eva_coverage md_gen sarif_gen mdr_register @@ -28,13 +28,13 @@ $(Report_markdown_DIR)/Report_markdown.mli: \ $(Report_markdown_DIR)/md_gen.mli \ $(Report_markdown_DIR)/Makefile echo "module Mdr_params: sig" > $@ - cat mdr_params.mli >> $@ + cat $(Report_markdown_DIR)/mdr_params.mli >> $@ echo "end" >> $@ echo "module Markdown: sig" >> $@ - cat markdown.mli >> $@ + cat $(Report_markdown_DIR)/markdown.mli >> $@ echo "end" >> $@ echo "module Md_gen: sig" >> $@ - cat md_gen.mli >> $@ + cat $(Report_markdown_DIR)/md_gen.mli >> $@ echo "end" >> $@ install:: -- GitLab