diff options
Diffstat (limited to 'otherlibs/labltk/browser/shell.ml')
| -rw-r--r-- | otherlibs/labltk/browser/shell.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/otherlibs/labltk/browser/shell.ml b/otherlibs/labltk/browser/shell.ml index e1de45134..13be2c3f9 100644 --- a/otherlibs/labltk/browser/shell.ml +++ b/otherlibs/labltk/browser/shell.ml @@ -257,10 +257,8 @@ let path_sep = if is_win32 then ";" else ":" let warnings = ref "Al" let program_not_found prog = - ignore begin - Jg_message.ask ~cancel:false ~no:false ~title:"Error" - ("Program \"" ^ String.escaped prog ^ "\"\nwas not found in path") - end + Jg_message.info ~title:"Error" + ("Program \"" ^ prog ^ "\"\nwas not found in path") let f ~prog ~title = let progargs = |