Rename `map_preimage` into `map_preimg` (to be consistent with `dom`).

For the domain of a map we use dom, not domain.

So it makes sense to also use img instead of image. In !444 (merged) we already do that for the proper image, so let's do too for the pre-image.

no strong opinion, I didn't even know we had map_preimg^^

resolved all threads

added 1 commit

• a2b4e045 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

enabled an automatic merge when the pipeline for a2b4e045 succeeds

@iris-users

• Rename map_preimage into map_preimg to be consistent with dom.

merged

mentioned in commit 2cf74f8b

mentioned in merge request !444 (merged)