remove Makefile

diff --git a/Makefile b/Makefile
deleted file mode 100644 (file)
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