diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 09b8c408a8..52f7b3d28a 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -73,3 +73,7 @@ let url_for_keyword = (Hashtbl.find ht : string -> string) +let browse_keyword text = + try + let u = url_for_keyword text in browse (current.doc_url ^ u) + with _ -> () |