diff options
Diffstat (limited to 'otherlibs/labltk/browser/main.ml')
| -rw-r--r-- | otherlibs/labltk/browser/main.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/labltk/browser/main.ml b/otherlibs/labltk/browser/main.ml index 55aa4be2f..a519e2c0a 100644 --- a/otherlibs/labltk/browser/main.ml +++ b/otherlibs/labltk/browser/main.ml @@ -21,7 +21,7 @@ let _ = let top = openTk class:"OCamlBrowser" () in Jg_config.init (); - bind top events:[[], `Destroy] action:(`Set ([], fun _ -> exit 0)); + bind top events:[`Destroy] action:(fun _ -> exit 0); at_exit Shell.kill_all; |