diff --git a/.Makefile.lint b/.Makefile.lint index aae7e04c6cece012878cb11252471af71e934e3b..fc916bfa1e33d42ff2e73b588b496e21b2d85da4 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