diff options
Diffstat (limited to 'otherlibs/labltk/browser/searchpos.ml')
| -rw-r--r-- | otherlibs/labltk/browser/searchpos.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/searchpos.ml b/otherlibs/labltk/browser/searchpos.ml index 5e45718fe..1f414686d 100644 --- a/otherlibs/labltk/browser/searchpos.ml +++ b/otherlibs/labltk/browser/searchpos.ml @@ -248,6 +248,7 @@ type module_widgets = let shown_modules = Hashtbl.create 17 let default_frame = ref None +let set_path = ref (fun _ ~sign -> assert false) let filter_modules () = Hashtbl.iter (fun key data -> @@ -335,6 +336,7 @@ let rec view_signature ?title ?path ?(env = !start_env) ?(detach=false) sign = view_module path ~env; find_shown_module path in + !set_path path ~sign; begin match mw.mw_title with None -> () | Some label -> Label.configure label ~text:title; |