• Show log

    Commit

  • Hash : 1db5b219
    Author : Edward Thomson
    Date : 2021-06-16T09:06:26

    filter: filter options are now "filter sessions"
    
    Filters use a short-lived structure to keep state during an operation to
    allow for caching and avoid unnecessary reallocations.  This was
    previously called the "filter options", despite the fact that they
    contain no configurable options.  Rename them to a "filter session" in
    keeping with an "attribute session", which more accurately describes
    their use (and allows us to create "filter options" in the future).