diff options
Diffstat (limited to 'lib/gmapl.mli')
| -rw-r--r-- | lib/gmapl.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/gmapl.mli b/lib/gmapl.mli index c3a55e8c1..23c77851b 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Maps from ['a] to lists of ['b]. *) |