You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Allow Idris to install IdrisDoc into a central location.
+ Default location is `<getDataDir>/docs`.
+ Flag `--info` has been updated to show doc location.
+ New flag `--installdoc <ipkg>` provided to install documentation
+ New flag `--docdir` provided to show documentation installation location.
+ New environment variable `IDRIS_DOC_PATH` to allow alternate means of customisation.
+ Installation for Idris' std libraries has been augmented to install library documentation as well.
0 commit comments