diff options
Diffstat (limited to 'otherlibs/dynlink/extract_crc.ml')
| -rw-r--r-- | otherlibs/dynlink/extract_crc.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/otherlibs/dynlink/extract_crc.ml b/otherlibs/dynlink/extract_crc.ml index 672ca6ea9..4a6a310a9 100644 --- a/otherlibs/dynlink/extract_crc.ml +++ b/otherlibs/dynlink/extract_crc.ml @@ -11,8 +11,6 @@ (* *) (***********************************************************************) -(* $Id$ *) - (* Print the digests of unit interfaces *) let load_path = ref [] |