mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 20:51:43 +03:00
Merge pull request #2836 from mattpolzin/library-data
[ new ] [ proposal ] Allow libraries to ship a data dir
This commit is contained in:
commit
ab0ff2754a
@ -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