diff --git a/collects/planet/config.ss b/collects/planet/config.ss index f444677cd8..cb8f3a1849 100644 --- a/collects/planet/config.ss +++ b/collects/planet/config.ss @@ -6,7 +6,9 @@ (PLANET-SERVER-NAME "planet.plt-scheme.org") (PLANET-SERVER-PORT 270) (PLANET-CODE-VERSION "300") - (PLANET-DIR (build-path (find-system-path 'addon-dir) "planet" (PLANET-CODE-VERSION))) + (PLANET-DIR (if (getenv "PLTPLANETDIR") + (string->path (getenv "PLTPLANETDIR")) + (build-path (find-system-path 'addon-dir) "planet" (PLANET-CODE-VERSION)))) (CACHE-DIR (build-path (PLANET-DIR) "cache")) (LINKAGE-FILE (build-path (PLANET-DIR) "LINKAGE")) (LOGGING-ENABLED? #t) diff --git a/collects/planet/doc.txt b/collects/planet/doc.txt index a326bae7c5..3261f423e9 100644 --- a/collects/planet/doc.txt +++ b/collects/planet/doc.txt @@ -52,8 +52,9 @@ Parameters: > (PLANET-DIR) -> directory-string > (PLANET-DIR directory-string) -> void -The root PLaneT directory. Default is the directory in which config.ss -is found. +The root PLaneT directory. If the environment variable PLTPLANETDIR is +set, default is its value; otherwise the default is the directory in +which config.ss is found. > (CACHE-DIR) -> directory-string > (CACHE-DIR directory-string) -> void