diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/Makefile.shared | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/Makefile.shared b/tools/Makefile.shared index 251743449..826accdf2 100644 --- a/tools/Makefile.shared +++ b/tools/Makefile.shared @@ -225,8 +225,7 @@ READ_CMT= \ ../typing/printtyp.cmo \ ../typing/mtype.cmo \ ../typing/envaux.cmo \ - ../typing/typedtreeMap.cmo \ - ../typing/typedtreeIter.cmo \ + ../typing/tast_mapper.cmo \ ../typing/cmt_format.cmo \ ../typing/stypes.cmo \ \ |