diff options
| author | Maxime Dénès | 2016-11-16 13:59:12 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-16 13:59:12 +0100 |
| commit | b072152fd5a1db47645981a2a0c542361da97420 (patch) | |
| tree | a44ba5953df5acc17b710e20426db115521de111 /dev | |
| parent | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff) | |
| parent | 1053c873bdaedf37c1fd35be4e7021bfc806c23d (diff) | |
Merge remote-tracking branch 'github/pr/361' into v8.6
Was PR#361: [doc] Mention XML protocol on changes.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 2 |
1 files changed, 2 insertions, 0 deletions
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, |