diff options
| -rw-r--r-- | tools/Makefile | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tools/Makefile b/tools/Makefile index 802494414..9bc1646ef 100644 --- a/tools/Makefile +++ b/tools/Makefile @@ -224,14 +224,6 @@ objinfo: objinfo.cmo clean:: rm -f objinfo -# Print imported interfaces for .cmi files - -intfinfo: intfinfo.cmo - $(CAMLC) $(LINKFLAGS) -o intfinfo config.cmo intfinfo.cmo - -clean:: - rm -f intfinfo - # Scan object files for required primitives PRIMREQ=primreq.cmo |