On Mon, 15 Jan 2024 17:44:10 GMT, Maurizio Cimadamore <mcimadamore at openjdk.org> wrote: > (we can probably tweak the name clash if the needs arise in a separate PR) Ok, I'll leave it like this then. ------------- PR Comment: https://git.openjdk.org/jextract/pull/175#issuecomment-1892585890