Commit 2023-01-05 07:04 5a3e8195
View on Github →feat(order/filter/basic): put pp_nodot attribute on filter.tendsto (#18062)
Make sure that tendsto f p q
is not pretty-printed as p.tendsto f q
, since this is not a property of p
but rather of f
.