diff options
Diffstat (limited to 'otherlibs/labltk/browser/searchpos.ml')
| -rw-r--r-- | otherlibs/labltk/browser/searchpos.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/searchpos.ml b/otherlibs/labltk/browser/searchpos.ml index 7b79fff5a..8cae99593 100644 --- a/otherlibs/labltk/browser/searchpos.ml +++ b/otherlibs/labltk/browser/searchpos.ml @@ -240,6 +240,8 @@ and search_pos_module m ~pos ~env = _, Pwith_type t -> search_pos_type_decl t ~pos ~env | _ -> () end + | Pmty_typeof md -> + () (* TODO? *) end end |