diff options
| author | ppedrot | 2011-11-29 18:47:28 +0000 |
|---|---|---|
| committer | ppedrot | 2011-11-29 18:47:28 +0000 |
| commit | b6e15ffb88bca689aa79b3d655cce986319188fd (patch) | |
| tree | 18443b4ea4f48d340c6f42e6cfece2a49b0d8960 | |
| parent | 091aa5db22acd7b7a7f214474bc20d85ada47379 (diff) | |
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
| -rw-r--r-- | toplevel/ide_intf.ml | 7 |
1 files 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) -> |