diff options
Diffstat (limited to 'otherlibs/labltk/browser/viewer.ml')
| -rw-r--r-- | otherlibs/labltk/browser/viewer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/labltk/browser/viewer.ml b/otherlibs/labltk/browser/viewer.ml index 6f8c8ca78..17c3ba584 100644 --- a/otherlibs/labltk/browser/viewer.ml +++ b/otherlibs/labltk/browser/viewer.ml @@ -400,7 +400,7 @@ class st_viewer ?(dir=Unix.getcwd()) ?on () = let label = Label.create tl ~anchor:`W ~padx:5 in let view = Frame.create tl in let buttons = Frame.create tl in - let all = Button.create buttons ~text:"Show all" ~padx:20 + let _all = Button.create buttons ~text:"Show all" ~padx:20 and close = Button.create buttons ~text:"Close all" ~command:close_all_views and detach = Button.create buttons ~text:"Detach" and edit = Button.create buttons ~text:"Impl" |