mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 02:23:44 +03:00
Added --mkdoc to CHANGELOG too
This commit is contained in:
parent
80aeecaac0
commit
980b6174ec
@ -170,6 +170,7 @@ Added
|
|||||||
|
|
||||||
* Lots of small performance improvements, some of which may be especially
|
* Lots of small performance improvements, some of which may be especially
|
||||||
noticeable in programs that do a lot of type level evaluation.
|
noticeable in programs that do a lot of type level evaluation.
|
||||||
|
* Added HTML documentation generation, using the `--mkdoc` flag
|
||||||
* Support for auto-completion in bash-like shells was added.
|
* Support for auto-completion in bash-like shells was added.
|
||||||
* Fixed case-splitting to respect any indentation there may be in the term being
|
* Fixed case-splitting to respect any indentation there may be in the term being
|
||||||
case-split and the surrounding symbols, instead of filtering out the
|
case-split and the surrounding symbols, instead of filtering out the
|
||||||
|
@ -130,7 +130,7 @@ Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler
|
|||||||
|
|
||||||
+ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
|
+ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
|
||||||
|
|
||||||
+ ``idris2 --mkdocs test.ipkg`` will generate HTML documentation for the
|
+ ``idris2 --mkdoc test.ipkg`` will generate HTML documentation for the
|
||||||
package, output to ``build/docs``
|
package, output to ``build/docs``
|
||||||
|
|
||||||
Once the test package has been installed, the command line option
|
Once the test package has been installed, the command line option
|
||||||
|
Loading…
Reference in New Issue
Block a user