PR !4#10230: chore: Delete some orphaned porting notes an...

Stream: triage

[Random Issue Bot]

Today I chose PR 10230 for discussion!

chore: Delete some orphaned porting notes and unnecessary noncomputable attributes
Created by @Matthew Robert Ballard (@mattrobball) on 2024-02-03
Labels: awaiting-review, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Matthew Ballard]

This seems pretty simple...

[Bryan Gin-ge Chen]

It looks like it fell off the #queue due to the merge conflict tag.

[Matthew Ballard]

Should be ahead of master now