From b1a22c6e7584dce2a8294cb29ddada39173ced8a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 27 Apr 2019 22:21:49 +0200
Subject: CoqIDE, cosmetic: removing obsolete comments.

There is no more uses of "old style preferences" but the comment was
still there.
---
 ide/preferences.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 57bc0f583f..3893d023bd 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -263,8 +263,6 @@ let get_unicode_bindings_default_file () =
 
 (** Hooks *)
 
-(** New style preferences *)
-
 let cmd_coqtop =
   new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string)
 
@@ -645,8 +643,6 @@ let tag_button () =
   let box = GPack.hbox () in
   new tag_button (Gobject.unsafe_cast box#as_widget)
 
-(** Old style preferences *)
-
 let save_pref () =
   if not (Sys.file_exists (Minilib.coqide_config_home ()))
   then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
-- 
cgit v1.2.3