aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 01aef20fc..ed52262af 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3127,7 +3127,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~callback:
(fun () ->
let av = session_notebook#current_term.analyzed_view in
- browse av#insert_message (!current.doc_url)) in
+ browse av#insert_message (doc_url ())) in
let _ = help_factory#add_item "Browse Coq _Library"
~callback:
(fun () ->