Make* class fixes (!845) · Merge requests · Iris / Iris · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/make2 into master 2 years ago

Activity

Ralf Jung mentioned in merge request !842 (closed) 2 years ago

mentioned in merge request !842 (closed)
Robbert Krebbers @robbertkrebbers · 2 years ago

Owner

Thanks for splitting the other MR!

LGTM.
Ralf Jung merged 2 years ago

merged
Ralf Jung mentioned in commit c2fd00b4 2 years ago

mentioned in commit c2fd00b4

Please register or sign in to reply