summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /ide/coqide.ml
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea2dfe4d..cc147d5e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *)
+(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
open Preferences
open Vernacexpr
@@ -3237,7 +3237,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~callback:
(fun () ->
let av = Option.get ((get_current_view ()).analyzed_view) in
- browse av#insert_message (!current.doc_url ^ "main.html")) in
+ browse av#insert_message (!current.doc_url)) in
let _ = help_factory#add_item "Browse Coq _Library"
~callback:
(fun () ->
@@ -3518,8 +3518,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let about_full_string =
"\nCoq is developed by the Coq Development Team\
\n(INRIA - CNRS - University Paris 11 and partners)\
- \nWeb site: http://coq.inria.fr\
- \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+ \nWeb site: " ^ Coq_config.wwwcoq ^
+ "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
\n\
\nCredits for CoqIDE, the Integrated Development Environment for Coq:\
\n\