aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cdglobals.ml
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-08 07:18:13 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-08 07:18:13 +0000
commit98f930742ca58742a9bc0a575e2d362ee2fa061e (patch)
treef58efb4683f29b725477a0b468c044875478a70f /tools/coqdoc/cdglobals.ml
parentd44af32d0946b62fe2db9efa47fb8b7063d0024d (diff)
Ajout d'options a coqdoc pour l'entete html
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10764 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cdglobals.ml')
-rw-r--r--tools/coqdoc/cdglobals.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index eef598fdd..44b9bd3ce 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -33,6 +33,10 @@ let close_out_file () = close_out !out_channel
let header_trailer = ref true
+let header_file = ref ""
+let header_file_spec = ref false
+let footer_file = ref ""
+let footer_file_spec = ref false
let quiet = ref true
let light = ref false
let gallina = ref false