Skip to content

After #3765 merges, use `div_floor() #3766

Open
Open
After #3765 merges, use `div_floor()#3766

Description

@larseggert
larseggert
opened on Jun 29, 2026

This should be div_floor() now. Or just /. (Not in this fix.)

Originally posted by @martinthomson in #3765 (comment)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    Priority

    None yet

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions