idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

Update changelog

Browse Source
This commit is contained in:
Christian Rasmussen 2020-06-17 05:06:07 +02:00
parent 21a1245c10
commit ceb7a30c09
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
CHANGELOG.md
View File

@ -34,6 +34,10 @@ Command-line options changes:
* Removed `--ide-mode-socket-with` option. `--ide-mode-socket` now accepts an
optional `host:port` argument.
* Added options to override source directory, build directory and output
directory: `--source-dir`, `--build-dir`, `--output-dir`.
+ These options are also available as fields in the package description:
`sourcedir`, `builddir`, `outputdir`.
Compiler changes: