mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
Allow libraries to ship a data dir at a standard location within their install directory.
This commit is contained in:
parent
947432fa30
commit
d53a277a34
@ -358,6 +358,7 @@ addDeps pkg = do
|
||||
| Failed errs => throw $ GenericMsg EmptyFC (printErrs pkg errs)
|
||||
log "package.depends" 10 $ "all depends: \{show allPkgs}"
|
||||
traverse_ addPackageDir allPkgs
|
||||
traverse_ addDataDir ((</> "data") <$> allPkgs)
|
||||
where
|
||||
-- Note: findPkgDir throws an error if a package is not found
|
||||
-- *unless* --ignore-missing-ipkg is enabled
|
||||
|
Loading…
Reference in New Issue
Block a user