summaryrefslogtreecommitdiff
path: root/config
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 /config
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'config')
-rw-r--r--config/coq_config.mli6
1 files changed, 5 insertions, 1 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 14595fa5..0dc4a6a8 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coq_config.mli 11858 2009-01-26 13:27:23Z notin $ i*)
+(*i $Id: coq_config.mli 12104 2009-04-24 18:10:10Z notin $ i*)
val local : bool (* local use (no installation) *)
@@ -45,4 +45,8 @@ val browser : string
(** default web browser to use, may be overriden by environment
variable COQREMOTEBROWSER *)
+val wwwcoq : string
+val wwwrefman : string
+val wwwstdlib : string
+
val has_natdynlink : bool