Skip to content

Commit

Permalink
[ doc ] moved --guarded lower in the CHANGELOG and fixed typo
Browse files Browse the repository at this point in the history
  • Loading branch information
Saizan committed May 19, 2021
1 parent ced2905 commit fd9680c
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,6 @@ Installation and infrastructure
Pragmas and options
-------------------

* New option `--guarded` turns on the Guarded Cubical extension of Agda.

See [Guarded Cubical](https://agda.readthedocs.io/en/v2.6.2/language/guaded-cubical.html)
in the documentation for more.

* New option `--auto-inline` turns on automatic compile-time inlining of simple
functions. This was previously enabled by default.

Expand Down Expand Up @@ -100,6 +95,11 @@ Pragmas and options
[#3026](https://github.com/agda/agda/issues/3026)), the
`--sized-types` flag can no longer be used while `--safe` is active.

* New option `--guarded` turns on the Guarded Cubical extension of Agda.

See [Guarded Cubical](https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html)
in the documentation for more.

Command-line interaction
------------------------

Expand Down

0 comments on commit fd9680c

Please sign in to comment.