add rename-by-pattern tactic (!218) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/rename-by-pat into master 4 years ago

All threads resolved!

rename_pat would be a shorter name, but OTOH this is more consistent with the existing select-style tactics so maybe that's the better choice.

Approval is optional

Activity

Ralf Jung added 1 commit 4 years ago
added 1 commit

8d2aa41e - add rename-by-pattern tactic

Compare with previous version
Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung
Last reply by Robbert Krebbers 4 years ago

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

+1

Ralf Jung resolved all threads 4 years ago

resolved all threads

Ralf Jung added 1 commit 4 years ago

added 1 commit

609de3aa - add rename-by-pattern tactic

Compare with previous version

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Ralf Jung added 1 commit 4 years ago

added 1 commit

0710439b - fmt

Compare with previous version

Ralf Jung resolved all threads 4 years ago

resolved all threads

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Looks good.

Robbert Krebbers merged 4 years ago

merged

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit 71b66d70

Please register or sign in to reply