diff options
Diffstat (limited to 'ide/blaster_window.ml')
| -rw-r--r-- | ide/blaster_window.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml index 83d900cc6e..d02243d118 100644 --- a/ide/blaster_window.ml +++ b/ide/blaster_window.ml @@ -49,16 +49,16 @@ class blaster_window (n:int) = let _ = view#set_rules_hint true in let col = GTree.view_column ~title:"Argument" () - ~renderer:(GTree.cell_renderer_text(), ["text",argument]) in + ~renderer:(GTree.cell_renderer_text [], ["text",argument]) in let _ = view#append_column col in let col = GTree.view_column ~title:"Tactics" () - ~renderer:(GTree.cell_renderer_text(), ["text",tactic]) in + ~renderer:(GTree.cell_renderer_text [], ["text",tactic]) in let _ = view#append_column col in let col = GTree.view_column ~title:"Status" () - ~renderer:(GTree.cell_renderer_toggle (), ["active",status]) in + ~renderer:(GTree.cell_renderer_toggle [], ["active",status]) in let _ = view#append_column col in let col = GTree.view_column ~title:"Delta Goal" () - ~renderer:(GTree.cell_renderer_text (), ["text",nb_goals]) in + ~renderer:(GTree.cell_renderer_text [], ["text",nb_goals]) in let _ = view#append_column col in let _ = GMisc.separator `HORIZONTAL ~packing:box1#pack () in |