From 039751853993cf426ae0a27eb26078ef3f96880d Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Thu, 9 May 2013 06:16:53 -0400 Subject: [PATCH] Fix inclusion of "keep-dirs.rktd". The file should be considered as source even though it's in the "doc" directory. --- collects/meta/dist-specs.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/collects/meta/dist-specs.rkt b/collects/meta/dist-specs.rkt index ca157f5fdc..abaeea7c11 100644 --- a/collects/meta/dist-specs.rkt +++ b/collects/meta/dist-specs.rkt @@ -169,8 +169,8 @@ gui-filter := (- (+ (collects: "**/gui/") (srcfile: "gui.rkt")) tools-filter := (+ (collects: "**/tools/") (srcfile: "tools.rkt")) ;; these are in the doc directory, but are committed in git and should be -;; considered like sources -std-docs := (doc: "doc-license.txt" "*-std/") +;; considered as sources +std-docs := (doc: "doc-license.txt" "keep-dirs.rktd" "*-std/") ;; ============================================================================ ;; Junk