agda/agda-pkg

install libraries in PATH: option --AGDA-DIR=PATH

Closed this issue · 1 comments

apkgbot commented
install libraries in PATH: option --AGDA-DIR=PATH
jonaprieto commented

I don't see now how to maintain this. We read from the config.py the location for Agda-DIR.
If I found the way to overwrite this value with the command init I'll open this again.