On 4/20/20 11:33 PM, Thomas Schwinge wrote:
> Really 'GOMP_MAP_DELETE', or should that rather be 'GOMP_MAP_RELEASE'?

Depends on the previous item, i.e. 'delete:' vs. 'release:/from:/…'

Rather obvious – OK?

Tobias

-----------------
Mentor Graphics (Deutschland) GmbH, Arnulfstraße 201, 80634 München / Germany
Registergericht München HRB 106955, Geschäftsführer: Thomas Heurung, Alexander Walter