diff options
Diffstat (limited to 'stdlib/filename.mli')
| -rw-r--r-- | stdlib/filename.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stdlib/filename.mli b/stdlib/filename.mli index 499e8bb291..e55469764c 100644 --- a/stdlib/filename.mli +++ b/stdlib/filename.mli @@ -11,7 +11,7 @@ (* *) (***********************************************************************) -(* $Id$ *) +(* $Id: filename.mli 12959 2012-09-27 13:12:51Z maranget $ *) (** Operations on file names. *) |