From b6e15ffb88bca689aa79b3d655cce986319188fd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 29 Nov 2011 18:47:28 +0000
Subject: Fixed a warning about unused variable introduced in r14731

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14743 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/ide_intf.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index c702eabb20..5987602127 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -359,11 +359,10 @@ let rec pr_setoptions opts =
 let pr_getoptions opts =
   let map (key, s) =
     let key = String.concat " " key in
-    s.opt_name
-(*     Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s" *)
-(*       key s.opt_sync s.opt_depr s.opt_name (*(pr_option_value s.opt_value)*) "" *)
+    Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n"
+      key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
   in
-  "\n  " ^ String.concat "\n  " (List.map map opts)
+  "\n" ^ String.concat "" (List.map map opts)
 
 let pr_call = function
   | Interp (r,b,s) ->
-- 
cgit v1.2.3