From: Mehdi Dogguy Date: Tue, 27 Apr 2010 13:10:54 +0200 Subject: [PATCH] Don't modify system files --- share/Makefile.dynamic | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic index e35b0b7..dbe5098 100644 --- a/share/Makefile.dynamic +++ b/share/Makefile.dynamic @@ -191,9 +191,9 @@ install:: $(CP) frama-c-$(PLUGIN_NAME).$(OCAMLBEST)$(EXE) \ $(BINDIR)/frama-c-$(PLUGIN_NAME)$(EXE); \ fi - $(PRINT_UPDATE) $(FRAMAC_SHARE)/known_plugins.ac - echo "ENABLE_`echo $(PLUGIN_NAME) | tr "a-z" "A-Z"`=$(PLUGIN_ENABLE)" \ - >> $(FRAMAC_SHARE)/known_plugins.ac +# $(PRINT_UPDATE) $(FRAMAC_SHARE)/known_plugins.ac +# echo "ENABLE_`echo $(PLUGIN_NAME) | tr "a-z" "A-Z"`=$(PLUGIN_ENABLE)" \ +# >> $(FRAMAC_SHARE)/known_plugins.ac ifeq ($(HAS_GUI),yes) $(PRINT_CP) $(PLUGIN_INSTALL_DIR)/gui $(CP) $(TARGETS_GUI) $(PLUGIN_INSTALL_DIR)/gui --