From eca4848e085a52c5a4d7d3f0d511b62e3e9ba70d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Mar 2018 10:01:03 -0300
Subject: Documenting the Export modifier for options in CHANGES.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 1c7c53f296..83f162c28c 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
 
-- 
cgit v1.2.3