1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 1c7c53f29..83f162c28 100644
--- a/CHANGES
+++ b/CHANGES
@@ -77,6 +77,9 @@ Vernacular Commands
 - Using “Require” inside a section is deprecated.
 - An experimental command "Show Extraction" allows to extract the content
   of the current ongoing proof (grant wish #4129).
+- The "Export" modifier can now be used when setting and unsetting options, and
+  will result in performing the same change when the module corresponding the
+  command is imported.
 
 Universes