From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 ide/preferences.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ide/preferences.mli')

diff --git a/ide/preferences.mli b/ide/preferences.mli
index 25535aa4..c3e26f50 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: preferences.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: preferences.mli 9240 2006-10-13 17:51:11Z notin $ i*)
 
 type pref =
     {
@@ -52,6 +52,8 @@ type pref =
       mutable use_utf8_notation : bool;
 *)
       mutable auto_complete : bool;
+      mutable stop_before : bool;
+      mutable lax_syntax : bool;
     }
 
 val save_pref : unit -> unit
-- 
cgit v1.2.3