Skip to content

add big_opM_gset_to_gmap

Ralf Jung requested to merge ralf/big_opM_gset_to_gmap into master

This can be quite useful e.g. when initializing a ghost_map with a gset_to_gmap.

Merge request reports