From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 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 d7f32380..6ee7918f 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 11009 2008-05-28 13:58:33Z jnarboux $ i*)
+(*i $Id$ i*)
 
 type pref =
     {
@@ -70,3 +70,5 @@ val change_font : ( Pango.font_description -> unit) ref
 val show_toolbar : (bool -> unit) ref
 val auto_complete : (bool -> unit) ref
 val resize_window : (unit -> unit) ref
+
+val use_default_doc_url : string
-- 
cgit v1.2.3