Skip to content

Commit

Permalink
[ changelog ] Write about new option
Browse files Browse the repository at this point in the history
  • Loading branch information
ice1000 committed Mar 24, 2020
1 parent f2205a3 commit 31bf313
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
Release notes for Agda version 2.6.2
====================================


Pragmas and options
-------------------

Expand All @@ -10,3 +9,9 @@ Pragmas and options
enabled, Agda will only consider candidates for instance search that
are in scope under an unqualified name (see
[#4522](https://github.com/agda/agda/pull/4522)).

* New option `--highlight-occurrences` (off by default) enables the HTML
backend to include a JavaScript file that highlights all occurrences of
the mouse-hovered symbol (see
[#4535](https://github.com/agda/agda/pull/4535)).

0 comments on commit 31bf313

Please sign in to comment.