list.v: avoid using mangled names (!180) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/mangle into master 4 years ago

All threads resolved!

This is needed to fix list.v compilation with name mangling enabled. I stopped after this file.

Activity

Ralf Jung @jung started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung
Last reply by Ralf Jung 4 years ago

Ralf Jung @jung started a thread on the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Thanks for this MR. I am happy to see that in a file of ~4600 lines only so much abuse of names appeared :)

Ralf Jung added 1 commit 4 years ago

added 1 commit

074b3315 - list.v: avoid using mangled names

Compare with previous version

Ralf Jung resolved all threads 4 years ago

resolved all threads

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Let's merge this then!

Robbert Krebbers merged 4 years ago

merged

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit de08bf75

Please register or sign in to reply