From 8a973cde918e3642812fa96aba05e84e2840950b Mon Sep 17 00:00:00 2001
From: Eli Barzilay <eli@barzilay.org>
Date: Sat, 15 May 2010 16:06:45 -0400
Subject: [PATCH] somehow this wasn't deleted earlier

---
 collects/meta/drdr/info.ss | 4 ----
 1 file changed, 4 deletions(-)
 delete mode 100644 collects/meta/drdr/info.ss

diff --git a/collects/meta/drdr/info.ss b/collects/meta/drdr/info.ss
deleted file mode 100644
index 6ae9ca135e..0000000000
--- a/collects/meta/drdr/info.ss
+++ /dev/null
@@ -1,4 +0,0 @@
-#lang setup/infotab
-
-(define name "DrDr")
-(define compile-omit-paths 'all)