From eca684b176e606b39bc0a1844cdb0e9e55f25113 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Nov 2007 09:11:50 +0000 Subject: [PATCH] removed dummy MATITA_CFLAGS assignement --- helm/software/matita/Makefile | 2 -- 1 file changed, 2 deletions(-) diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index e10692b17..ad5a18892 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -236,8 +236,6 @@ cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt) ifeq ($(DISTRIBUTED),yes) -MATITA_CFLAGS = #-nodb - dist_library: install_preliminaries dist_library@standard-library dist_library@%: $(H)echo "MATITAMAKE init $*" -- 2.39.2