diff options
| author | Gaëtan Gilbert | 2020-02-24 15:03:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | 8e3abd852c9a1c65738be63215e94014550f2c5a (patch) | |
| tree | 1cdd4d19b7a1e8cc828cc608ac8c6f56dffebe9e /library/libobject.mli | |
| parent | b98ef72ee300e52dd2c67f03da358e3c2102cdbb (diff) | |
correctly open objects for Names filters
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/libobject.mli b/library/libobject.mli index 27b47264a6..1c82349bb6 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -92,7 +92,7 @@ val filter_and : open_filter -> open_filter -> open_filter option val filter_or : open_filter -> open_filter -> open_filter -val todo_filter : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit +val in_filter_ref : Names.GlobRef.t -> open_filter -> bool (** The default object is a "Keep" object with empty methods. Object creators are advised to use the construction |