aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.mli
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-26 13:55:07 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-26 13:55:07 +0000
commite4b85d5e575c684df24ad7259207a185c5d5e179 (patch)
tree90e95b9db4aaf4b27f6b698628c0d99c3422f95e /toplevel/usage.mli
parent9cdf9c3c0341a395249946d9e8f0bed7dd3c6d53 (diff)
- Suppression date dans configure du trunk
- Utilisation de get_version_date pour l'option -v (plutôt que la date non à jour du configure) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11714 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/usage.mli')
-rw-r--r--toplevel/usage.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index fb973e3ba..37d96cfa8 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -21,3 +21,6 @@ val print_usage_coqc : unit -> unit
(*s Prints the configuration information *)
val print_config : unit -> unit
+
+(*s Prints the header *)
+val print_header : unit -> unit