aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES6
1 files changed, 6 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 6515d5d0f..f5e83bdae 100644
--- a/CHANGES
+++ b/CHANGES
@@ -194,6 +194,12 @@ Internal Infrastructure
by option -vmbyteflags which expects a comma-separated argument.
* The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
+Miscellaneous
+
+- ML plugins now require a "DECLARE PLUGIN \"foo\"" statement. The "foo" name
+ must be exactly the name of the ML module that will be loaded through a
+ "Declare ML \"foo\"" command.
+
Changes from V8.4beta2 to V8.4
==============================