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)