From 9b043ecce5efa63c7c58ef957027e094d98d16a6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Apr 2013 12:35:37 +0200 Subject: [PATCH] remove Makefile --- Makefile | 38 -------------------------------------- 1 file changed, 38 deletions(-) delete mode 100644 Makefile diff --git a/Makefile b/Makefile deleted file mode 100644 index 6d83fd2..0000000 --- a/Makefile +++ /dev/null @@ -1,38 +0,0 @@ -PACKAGE=cost-plug-in -VERSION=0.1 -PACKAGE_RES=$(PACKAGE)-$(VERSION).tgz - -JESSIE=frama-c_jessie - -all: - make -C plugin - make -C wrapper - -install: - mkdir -p /usr/local/bin - cp $(JESSIE) /usr/local/bin - make -C plugin install - make -C wrapper install - -clean: - rm -fr $(PACKAGE) $(PACKAGE_RES) doc - make -C plugin clean - make -C wrapper clean - -distclean: clean - make -C plugin distclean - make -C wrapper distclean - -dist: - rm -fr $(PACKAGE) $(PACKAGE_RES) - mkdir $(PACKAGE) - for i in `cat distributed_files` doc/html/*.html; do \ - if test -f $$i; then \ - cp -fr --parents $$i $(PACKAGE); \ - else \ - mkdir -p $$i; \ - fi; \ - done - tar cvfz $(PACKAGE_RES) $(PACKAGE) - -.PHONY = install clean distclean dist -- 2.39.2