aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/index.mli
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
commit62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch)
treee4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /tools/coqdoc/index.mli
parent97da8221e0097ed365f0a99e4960148424a59734 (diff)
Added checksums to glob files and warned about possibly missing
packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/index.mli')
-rw-r--r--tools/coqdoc/index.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index a5430f5f1..bb775d261 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -52,7 +52,7 @@ val add_external_library : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
-val read_glob : string -> unit
+val read_glob : Digest.t option -> string -> unit
(*s Indexes *)