From 1053c873bdaedf37c1fd35be4e7021bfc806c23d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 16 Nov 2016 11:17:39 +0100
Subject: [doc] Mention XML protocol on changes.

It may be worth it, also added a note about file reorganization.
---
 dev/doc/changes.txt | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 79a0c6312a..d052468f99 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -14,6 +14,8 @@ kernel/closure.ml{,i} -> kernel/cClosure.ml{,i}
 lib/errors.ml{,i} -> lib/cErrors.ml{,i}
 toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i}
 
+All IDE-specific files, including the XML protocol have been moved to ide/
+
 ** Reduction functions **
 
 In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,
-- 
cgit v1.2.3