diff options
Diffstat (limited to 'lib/bstack.mli')
| -rw-r--r-- | lib/bstack.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/bstack.mli b/lib/bstack.mli index d1f9ae387..fc646f1a4 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (* Bounded stacks. If the depth is [None], then there is no depth limit. *) |