removed $id
This commit is contained in:
parent
d46c2e651c
commit
d39755d9a4
3 changed files with 0 additions and 6 deletions
|
@ -7,8 +7,6 @@
|
|||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
open Format
|
||||
open List
|
||||
open Modules
|
||||
|
|
|
@ -7,8 +7,6 @@
|
|||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
open Format
|
||||
open List
|
||||
open Misc
|
||||
|
|
|
@ -8,8 +8,6 @@
|
|||
(**************************************************************************)
|
||||
(* Object code internal representation *)
|
||||
|
||||
(* $Id$ *)
|
||||
|
||||
open Misc
|
||||
open Names
|
||||
open Ident
|
||||
|
|
Loading…
Reference in a new issue