finding what happened to an identifier

Stream: general

[Scott Morrison]

I'm trying to update a branch to work with current mathlib, and an identifier has gone missing, presumably renamed in the meantime. Can someone suggest a helpful git incantation which will show me the commit in which that identifier was removed? I'm particularly looking at fin.le_iff_val_le_val at the moment (which seems to have been replaced by fin.le_iff_coe_le_coe).

[Scott Morrison]

(And I know from git blame that that happened in #4925 --- but how would I have done this if I hadn't stumbled upon the replacement?)

[Alex J. Best]

I use git log -Sstring

[Alex J. Best]

which gives log entries that contain "string" in their diff

[Bryan Gin-ge Chen]

Right, from that command, I think the PR that made the change was actually #3955: diff that hopefully highlights the change

[Bryan Gin-ge Chen]

Ugh, I guess not, since data/fin.lean is collapsed. Anyways, it's lines 233 on the left and 249 on the right.