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