From 43fb4494aeb550453d95b8c82e2c92772f3106a7 Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Thu, 16 Jun 2005 00:35:53 +0000 Subject: [PATCH] forgot to remove makefile svn: r190 --- collects/mztake/makefile | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 collects/mztake/makefile diff --git a/collects/mztake/makefile b/collects/mztake/makefile deleted file mode 100644 index 75f8c7b007..0000000000 --- a/collects/mztake/makefile +++ /dev/null @@ -1,12 +0,0 @@ -all: - setup-plt -p -l mztake - setup-plt -l frtime - setup-plt -l stepper - -plt: - mred -u make-plt.ss - mv *.plt ../../web/files/ - -clean: - ${RM} -r compiled private/compiled - ${RM} *distro*