diff options
Diffstat (limited to 'otherlibs/labltk')
| -rw-r--r-- | otherlibs/labltk/browser/searchpos.ml | 7 | ||||
| -rw-r--r-- | otherlibs/labltk/lib/Makefile | 2 |
2 files changed, 1 insertions, 8 deletions
diff --git a/otherlibs/labltk/browser/searchpos.ml b/otherlibs/labltk/browser/searchpos.ml index f6fb50051b..78087c80d9 100644 --- a/otherlibs/labltk/browser/searchpos.ml +++ b/otherlibs/labltk/browser/searchpos.ml @@ -693,13 +693,6 @@ and search_pos_class_structure ~pos cls = | Cf_val (_, _, Some exp, _) -> search_pos_expr exp ~pos | Cf_val _ -> () | Cf_meth (_, exp) -> search_pos_expr exp ~pos - | Cf_let (_, pel, iel) -> - List.iter pel ~f: - begin fun (pat, exp) -> - search_pos_pat pat ~pos ~env:exp.exp_env; - search_pos_expr exp ~pos - end; - List.iter iel ~f:(fun (_,exp) -> search_pos_expr exp ~pos) | Cf_init exp -> search_pos_expr exp ~pos end diff --git a/otherlibs/labltk/lib/Makefile b/otherlibs/labltk/lib/Makefile index 6be9af0560..35ba8ff680 100644 --- a/otherlibs/labltk/lib/Makefile +++ b/otherlibs/labltk/lib/Makefile @@ -71,7 +71,7 @@ $(LIBNAME)top$(EXE) : $(TOPDEPS) $(LIBNAME).cma ../support/lib$(LIBNAME).$(A) $(LIBNAME): Makefile $(TOPDIR)/config/Makefile @echo Generate $@ @echo "#!/bin/sh" > $@ - @echo 'exec $(INSTALLDIR)/$(LIBNAME)top$(EXE) -I $(INSTALLDIR) $$*' >> $@ + @echo 'exec $(INSTALLDIR)/$(LIBNAME)top$(EXE) -I $(INSTALLDIR) "$$@"' >> $@ install-script: $(LIBNAME) cp $(LIBNAME) $(BINDIR) |