From f9e3b09069c3e13214745e095edbb8925a7844a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 15 Mar 2019 18:16:02 +0100 Subject: [PATCH] [lint] reverting print-dynamic-api --- .Makefile.lint | 1 - 1 file changed, 1 deletion(-) diff --git a/.Makefile.lint b/.Makefile.lint index aae7e04c6ce..fc916bfa1e3 100644 --- a/.Makefile.lint +++ b/.Makefile.lint @@ -357,7 +357,6 @@ ML_LINT_KO+=src/plugins/pdg_types/pdgTypes.mli ML_LINT_KO+=src/plugins/postdominators/compute.ml ML_LINT_KO+=src/plugins/postdominators/postdominators_parameters.ml ML_LINT_KO+=src/plugins/postdominators/print.ml -ML_LINT_KO+=src/plugins/print_api/dynamic_plugins.mli ML_LINT_KO+=src/plugins/print_api/print_interface.ml ML_LINT_KO+=src/plugins/scope/Scope.mli ML_LINT_KO+=src/plugins/scope/datascope.ml -- GitLab