fix info-domain updating to recognize "info.ss" in addition to "info.rkt"
which solves the problem of forgetting a Planet-based tool when a new Planet-based tool is installed (if the old tool used "info.ss" instead of "info.rkt")
This commit is contained in:
parent
20bb4a8dfa
commit
cdf67d884f
|
@ -723,12 +723,11 @@
|
|||
(and (if (cc-root-dir cc)
|
||||
(relative-path? p)
|
||||
(complete-path? p))
|
||||
(file-exists?
|
||||
(build-path
|
||||
(if (cc-root-dir cc)
|
||||
(let ([dir (if (cc-root-dir cc)
|
||||
(build-path (cc-root-dir cc) p)
|
||||
p)
|
||||
"info.rkt"))))))
|
||||
p)])
|
||||
(or (file-exists? (build-path dir "info.rkt"))
|
||||
(file-exists? (build-path dir "info.ss"))))))))
|
||||
a)
|
||||
(list (? symbol? b) ...)
|
||||
c
|
||||
|
|
Loading…
Reference in New Issue
Block a user