diff options
Diffstat (limited to 'toplevel/usage.mli')
| -rw-r--r-- | toplevel/usage.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 1dfd4897b..23e807c16 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Prints the version number on the standard output and exits (with 0). } *) val version : unit -> 'a |