Rename instance `finmap_lookup_total` → `map_lookup_total`. (!220) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/map_lookup_total into master 4 years ago

This this is an instance, not a definition, it should not affect anyone.

Activity

Robbert Krebbers added 1 commit 4 years ago
added 1 commit

7bb734bc - Rename instance `finmap_lookup_total` → `map_lookup_total`.

Compare with previous version
Ralf Jung @jung · 4 years ago

Owner

rg agrees that there are no users. Should we still have a changelog entry?
Robbert Krebbers @robbertkrebbers · 4 years ago

Author Owner

Don't think so, instances names should be internal.
Robbert Krebbers merged 4 years ago

merged
Robbert Krebbers mentioned in commit 9f3e4929 4 years ago

mentioned in commit 9f3e4929

Please register or sign in to reply