From 2e9e6e8c694cb2bfec9c2fb58053cd270f135796 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Jul 2014 14:22:12 +0200
Subject: Documenting the need of the "DECLARE PLUGIN" statement.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 6515d5d0f0..f5e83bdaed 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
 ==============================
 
-- 
cgit v1.2.3