Fix inclusion of "keep-dirs.rktd".
The file should be considered as source even though it's in the "doc"
directory.
(cherry picked from commit 0397518539
)
This commit is contained in:
parent
3c9428e434
commit
e6912bd39c
|
@ -171,8 +171,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
|
||||
|
|
Loading…
Reference in New Issue
Block a user