diff options
Diffstat (limited to 'interp/smartlocate.ml')
| -rw-r--r-- | interp/smartlocate.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index faad3c50a..424e7cc1e 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -11,8 +11,6 @@ (* This file provides high-level name globalization functions *) -(* $Id:$ *) - (* *) open Pp open Util |