From c53f2f75375dfffd2f258c76f5b722d37ab0daf9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 26 Aug 2015 00:47:26 +0200
Subject: Switching to an event-based mechanism for CoqIDE preferences.

There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
---
 ide/ide.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/ide.mllib')

diff --git a/ide/ide.mllib b/ide/ide.mllib
index e082bd18c..83b314283 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,6 @@ Configwin
 Editable_cells
 Config_parser
 Tags
-Wg_Segment
 Wg_Notebook
 Config_lexer
 Utf8_convert
@@ -21,6 +20,7 @@ Coq
 Coq_lex
 Sentence
 Gtk_parsing
+Wg_Segment
 Wg_ProofView
 Wg_MessageView
 Wg_Detachable
-- 
cgit v1.2.3