diff options
Diffstat (limited to 'otherlibs/labltk/browser')
| -rw-r--r-- | otherlibs/labltk/browser/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/Makefile b/otherlibs/labltk/browser/Makefile index d1da76bd6..bcc67c51a 100644 --- a/otherlibs/labltk/browser/Makefile +++ b/otherlibs/labltk/browser/Makefile @@ -55,5 +55,6 @@ dummy.mli: rm -f $@ ln -s dummyUnix.mli $@ shell.cmo: dummy.cmi +lexical.cmi searchid.cmi typecheck.cmi: $(TOPDIR)/toplevel/toplevellib.cma include .depend |