mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-19 21:17:51 +03:00
7f0a137c7a
Idris' output has been updated to more accurately reflect its progress through the compiler i.e. Type Checking; Totality Checking; IBC Generation; Compiling; and Code Generation. To control the loudness of the reporting three verbosity levels are introduced: `--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose` have been retained. |
||
---|---|---|
.. | ||
idris.1 |