diff options
Diffstat (limited to 'stdlib/marshal.mli')
| -rw-r--r-- | stdlib/marshal.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stdlib/marshal.mli b/stdlib/marshal.mli index 86e1ebd199..0f6de83134 100644 --- a/stdlib/marshal.mli +++ b/stdlib/marshal.mli @@ -11,7 +11,7 @@ (* *) (***********************************************************************) -(* $Id$ *) +(* $Id: marshal.mli 12858 2012-08-10 14:45:51Z maranget $ *) (** Marshaling of data structures. |